anchor.diff:  
   and translate (env:Env.env) (bs:list<t>) (e:term) : t =
       match (SS.compress e).n with
  -    | Tm_delayed _ -> failwith "Tm_delayed: Impossible"
  -
  -    | Tm_unknown _ -> failwith "Tm_unknown: Impossible"
  +    | Tm_delayed (_, _) -> failwith "Tm_delayed: Impossible"
  +
  +    | Tm_unknown -> failwith "Tm_unknown: Impossible"
   
       | Tm_constant (FStar.Const.Const_unit) ->
         Unit
  
positive.code: //IN F*: and t : Type0 =
  and t = //JUST FSHARP
    | Lam of (t -> t) * aqual
    | Accu of atom * list<t * aqual>
    (* For simplicity represent constructors with fv as in F* *)
    | Construct of fv * list<t * aqual> (* Zoe: This is used for both type and data constructors*)
    | Unit
    | Bool of bool
  
  
negative.code: open FStar.All
  open FStar
  open FStar.TypeChecker
  open FStar.TypeChecker.Env
  open FStar.Syntax.Syntax
  open FStar.Ident
  
  