anchor.diff:  type atom = //JUST FSHARP
     | Var of var
     | Match of t * (* the scutinee *)
  -             (t -> t) (* the closure that pattern matches the scrutiny *)
  -             //NS: add a thunked pattern translations here
  +             (t -> t) * (* the closure that pattern matches the scrutiny *)
  +             list<branch> 
  +             // ZP: Keep the original branches to reconstruct just the patterns
  +             // NS: add a thunked pattern translations here ZP: Not entirely sure that this is needed, trying something simpler first.
  +             
     | Rec of letbinding * list<letbinding> * list<t> (* Danel: This wraps a unary F* rec. def. as a thunk in F# *)
     (* Zoe : a recursive function definition together with its block of mutually recursive function definitions and its environment *)
   //IN F*: and t : Type0 =
  
positive.code:   | Accu _ -> true
    | _ -> false
  
  let rec pickBranch (scrut : t) (branches : list<branch>) : option<(term * list<t>)>  =
      //NS: adapted from FStar.TypeChecker.Normalize: rebuild_match
      let rec matches_pat (scrutinee:t) (p:pat)
          : BU.either<list<t>, bool> =
  
negative.code: and atom_to_string (a: atom) =
      match a with
      | Var v -> "Var " ^ (P.bv_to_string v)
      | Match (t, _, _) -> "Match " ^ (t_to_string t)
      | Rec (_,_, l) -> "Rec (" ^ (String.concat "; " (List.map t_to_string l)) ^ ")"
  
  let is_not_accu (x:t) =
  