anchor.diff:  
     let ret_tot_type0 = Some (Inl (U.lcomp_of_comp <| S.mk_Total U.ktype0)) in
     let mk_forall (x: S.bv) (body: S.term): S.term =
  -    let tforall = U.mk_app (S.mk_Tm_uinst U.tforall [ U_unknown ]) [ S.as_arg x.sort ] in
  -    S.mk (Tm_app (tforall, [ S.as_arg (U.abs [ S.mk_binder x ] body ret_tot_type0)])) None Range.dummyRange
  +    S.mk (Tm_app (U.tforall, [ S.as_arg (U.abs [ S.mk_binder x ] body ret_tot_type0)])) None Range.dummyRange
     in
   
     (* For each (target) type t, we define a binary relation in t called ≤_t.
  
positive.code:     let wp1 = S.gen_bv "wp1" None wp_a in
      let wp2 = S.gen_bv "wp2" None wp_a in
      let body = mk_leq wp_a (S.bv_to_name wp1) (S.bv_to_name wp2) in
      U.abs (S.binders_of_list [ wp1; wp2 ]) body ret_tot_type0
    in
    check env "stronger" (U.abs (binders @ [ S.mk_binder a ]) stronger None);
  
    let null_wp = snd ed.null_wp in
  
  
negative.code:       d str;
        Util.print2 "Generated term for %s: %s\n" str (Print.term_to_string t);
        let t, { res_typ = res_typ }, _ = tc_term env t in
        let res_typ = normalize env res_typ in
        Util.print2 "Inferred type for %s: %s\n" str (Print.term_to_string res_typ)
      end
    in
  
  