anchor.diff:                  let sub_probs, tcs, f = aux scope args qs in
                   let f = match bopt with
                       | None ->
  -                      U.mk_conj_l (f:: (probs |> List.map (fun prob -> p_guard prob |> fst)))
  +                      let f = U.mk_conj_l (f:: (probs |> List.map (fun prob -> p_guard prob |> fst))) in
  +                      def_check_closed (p_loc orig) "imitation_sub_probs (1)" f;
  +                      f
                       | Some b ->
                         let u_b = env.universe_of env (fst b).sort in
  -                      U.mk_conj_l (U.mk_forall u_b (fst b) f :: (probs |> List.map (fun prob -> p_guard prob |> fst))) in
  +                      let f = U.mk_conj_l (U.mk_forall u_b (fst b) f :: (probs |> List.map (fun prob -> p_guard prob |> fst))) in
  +                      def_check_closed (p_loc orig) "imitation_sub_probs (2)" f;
  +                      f
  +                in
   
                   probs@sub_probs, tc::tcs, f in
   
  
positive.code:     | T (t, _) -> as_arg t
      | _ -> failwith "Impossible"
  
  let imitation_sub_probs orig env scope (ps:args) (qs:list<(option<binder> * variance * tc)>) =
     //U p1..pn REL h q1..qm
     //if h is not a free variable
     //extend_subst: (U -> \x1..xn. h (G1(x1..xn), ..., Gm(x1..xm)))
  
negative.code: (* <solving problems>                               *)
  (* ------------------------------------------------ *)
  
  let u_abs (k : typ) (ys : binders) (t : term) : term =
      let (ys, t), (xs, c) = match (SS.compress k).n with
          | Tm_arrow(bs, c) ->
            if List.length bs = List.length ys
  