anchor.diff:  //IN F*: type atom : Type0 =
   type atom = //JUST FSHARP
     | Var of var
  -  | Sort of sort (* for full CiC -- not used right now *)
  -  | Prod of t * t (* for full CiC -- not used right now *)
  +  | Type of universe
     | Match of t * (* the scutinee *)
                (t -> t) (* the closure that pattern matches the scrutiny *) 
     | Rec of letbinding * list<t> (* Danel: This wraps a unary F* rec. def. as a thunk in F# *)
   //IN F*: and t : Type0 =
   and t = //JUST FSHARP
     | Lam of (t -> t)
  -  | Fix of (t -> t) (* potentially recursive (i.e. a lambda inside ). The only difference with [Lam] is that there is an [is_accu] for the argument during application *)
     | Accu of atom * list<t>
     (* For simplicity represent constructors with fv as in F* *)
     | Construct of fv * list<t>
  
positive.code: 
      | Tm_uinst _ -> debug_term e; failwith "Tm_uinst: Not yet implemented"
  
      | Tm_type u -> debug_term e; failwith "Tm_type: Not yet implemented"
  
      | Tm_arrow (bs, c) -> debug_term e; failwith "Tm_arrow: Not yet implemented"
  
  
negative.code: let mkAccuVar (v:var) = Accu(Var v, [])
  let mkAccuMatch (s : t) (c : t -> t) = Accu(Match (s, c), [])
  let mkAccuRec (b:letbinding) (env:list<t>) = Accu(Rec(b, env), [])
  let mkAccTyp (u:universe) = Accu(Type u, [])
  
  let isAccu (trm:t) = 
    match trm with 
  