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:     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 (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
    // Not registering this one at top-level... not strictly needed. We'll inline
    // the definition. (Also: registering it at top-level triggers a universes
    // issue.) Also, note that this term does _not_ abstract of [binders]. This is
    // ok, because [tc_eff_decl] will close [binders].
    check env "wp_if_then_else" (U.abs binders wp_if_then_else None);
  
    (* val st2_assert_p : heap:Type ->a:Type -> q:Type0 -> st2_wp heap a ->
                         Tot (st2_wp heap a)
  
negative.code:   // [wp_a] has been type-checked and contains universe unification variables;
    // we want to re-use [wp_a] and make it re-generalize accordingly
    let wp_a = N.normalize [N.Beta; N.EraseUniverses] env wp_a in
    let a = { a with sort = N.normalize [ N.EraseUniverses ] env a.sort } in
  
    (* A series of macros and combinators to automatically build WP's. In these
     * definitions, both [binders] and [a] are opened. This means that macros
  