anchor.diff:    let env, c_push = register env (mk_lid "push") c_push in
   
     let ret_tot_wp_a = Some (Inl (U.lcomp_of_comp (mk_Total wp_a))) in
  +  let mk_generic_app c =
  +    if List.length binders > 0 then
  +      mk (Tm_app (c, args_of_binders binders))
  +    else
  +      c
  +  in
   
     (* val st2_if_then_else : heap:Type -> a:Type -> c:Type0 ->
                               st2_wp heap a -> st2_wp heap a ->
  
positive.code:   // Making the assumption that the thing we're passed is a top-level name.
    match (SS.compress (N.normalize [ N.EraseUniverses ] env.env t)).n with
    | Tm_fvar { fv_name = lid } ->
        let t = N.normalize [ N.UnfoldUntil Delta_constant; N.NoInline ] env.env t in
        Util.print1 "Recording definition of %s\n" (text_of_lid lid.v);
        let keep, ret = f env t in
        { env with definitions = (lid.v, keep) :: env.definitions }, ret
  
negative.code:     let st2_if_then_else heap a c = st2_liftGA2 (l_ITE c) *)
    let wp_if_then_else =
      let c = S.gen_bv "c" None U.ktype in
      U.abs (binders @ S.binders_of_list [ a; c ]) (
        let l_ite = fvar Const.ite_lid (S.Delta_unfoldable 2) None in
        U.mk_app c_lift2 (List.map S.as_arg [
          U.mk_app l_ite [S.as_arg (S.bv_to_name c)]
        ])
      ) ret_tot_wp_a
    in
    let env, wp_if_then_else = register env (mk_lid "wp_if_then_else") wp_if_then_else in
    let wp_if_then_else = mk_generic_app wp_if_then_else in
  
    (* val st2_assert_p : heap:Type ->a:Type -> q:Type0 -> st2_wp heap a ->
                         Tot (st2_wp heap a)
  