anchor.diff:                    Tot (st2_gctx heap a t2)
       let st2_app #heap #a #t1 #t2 l r = fun p h -> l p h (r p h) *)
     let c_app =
  -    let t1 = S.gen_bv "t1" None U.ktype in
  -    let t2 = S.gen_bv "t2" None U.ktype in
  +    let t1 = S.gen_bv "t1" None U.ktype0 in
  +    let t2 = S.gen_bv "t2" None U.ktype0 in
       let l = S.gen_bv "l" None (mk_gctx
         (U.arrow [ S.mk_binder (S.new_bv None (S.bv_to_name t1)) ] (S.mk_GTotal (S.bv_to_name t2))))
       in
       let r = S.gen_bv "r" None (mk_gctx (S.bv_to_name t1)) in
       let ret = Some (Inl (U.lcomp_of_comp (mk_Total (mk_gctx (S.bv_to_name t2))))) in
       let outer_body =
  -      let gamma_as_args = args_of_bv gamma in
  +      let gamma_as_args = args_of_binders gamma in
         let inner_body =
           U.mk_app
             (S.bv_to_name l)
             (gamma_as_args @ [ S.as_arg (U.mk_app (S.bv_to_name r) gamma_as_args)])
         in
  -      U.abs (mk_all_implicit gamma) inner_body ret
  -    in
  -    U.abs (binders_of_list [ t1, true; t2, true; l, false; r, false ]) outer_body ret
  -  in
  -  check env "app" (U.abs (binders @ [ S.mk_binder a ]) c_app None);
  +      U.abs gamma inner_body ret
  +    in
  +    U.abs (mk_all_implicit binders @ binders_of_list [ a, true; t1, true; t2, true; l, false; r, false ]) outer_body ret
  +  in
  +  let env, c_app = register env (mk_lid "app") c_app in
   
     (* val st2_liftGA1 : #heap:Type -> #a:Type -> #t1:Type -> #t2:Type ->
                          f : (t1 -> GTot t2) ->
  
positive.code:     let l_and = fvar Const.and_lid (S.Delta_unfoldable 1) None in
      let body =
        U.mk_app c_app (List.map S.as_arg [
          unknown; unknown;
          U.mk_app c_pure (List.map S.as_arg [
            unknown;
            U.mk_app l_and [S.as_arg (S.bv_to_name q)]]);
          S.bv_to_name wp])
      in
  
negative.code:     let l_imp = fvar Const.imp_lid (S.Delta_unfoldable 1) None in
      let body =
        U.mk_app c_app (List.map S.as_arg [
          U.mk_app c_pure (List.map S.as_arg [
            U.mk_app l_imp [S.as_arg (S.bv_to_name q)]]);
          S.bv_to_name wp])
      in
  