anchor.diff:      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
  
positive.code:                         Tot (st2_wp heap a)
      let st2_close_wp heap a b f = st2_app (st2_pure l_Forall) (st2_push f) *)
    let wp_close =
      let b = S.gen_bv "b" None U.ktype in
      let t_f = U.arrow [ S.null_binder (S.bv_to_name b) ] (S.mk_Total wp_a) in
      let f = S.gen_bv "f" None t_f 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;
            tforall]);
          U.mk_app c_push (List.map S.as_arg [
            unknown; unknown;
            S.bv_to_name f])])
      in
      U.abs (S.binders_of_list [ a; b; f ]) body ret_tot_wp_a
    in
  
negative.code:     let a1 = S.gen_bv "a1" None (mk_gctx (S.bv_to_name t1)) in
      let a2 = S.gen_bv "a2" None (mk_gctx (S.bv_to_name t2)) in
      let ret = Some (Inl (U.lcomp_of_comp (mk_Total (mk_gctx (S.bv_to_name t3))))) in
      U.abs (binders @ binders_of_list [ a, true; t1, true; t2, true; t3, true; f, false; a1, false; a2, false ]) (
        U.mk_app c_app (List.map S.as_arg [
          U.mk_app c_app (List.map S.as_arg [
            U.mk_app c_pure (List.map S.as_arg [ S.bv_to_name f ]);
            S.bv_to_name a1 ]);
          S.bv_to_name a2 ])
      ) ret
    in
    let env, c_lift2 = register env (mk_lid "lift2") c_lift2 in
  
    (* val st2_push : #heap:Type -> #a:Type -> #t1:Type -> #t2:Type ->
                      f:(t1 -> Tot (st2_gctx heap a t2)) ->
                      Tot (st2_ctx heap a (t1->GTot t2))
      let st2_push #heap #a #t1 #t2 f = fun p h e1 -> f e1 p h *)
    let c_push =
      let t1 = S.gen_bv "t1" None U.ktype0 in
      let t2 = S.gen_bv "t2" None U.ktype0 in
      let t_f = U.arrow
        [ S.null_binder (S.bv_to_name t1) ]
        (S.mk_Total (mk_gctx (S.bv_to_name t2)))
  