anchor.diff:      | Tm_uvar (u, _) -> u
       | _ -> failwith "Not a flex-uvar"
   
  -(* Make sure the uvar at the head of t0 is not affected by a
  - * the substitution in the Tm_uvar node.
  +(* ensure_no_uvar_subst: Make sure the uvar at the head of t0 is not
  + * affected by a the substitution in the Tm_uvar node.
    *
    * In the case that it is, first solve it to a new appropriate uvar
    * without a substitution. This function returns t again, though it is
  
positive.code:        *
         * See issue #1616. *)
          let t1, wl = ensure_no_uvar_subst t1 wl in
          let t2, wl = ensure_no_uvar_subst t2 wl in
          let f1 = destruct_flex_t' t1 in
          let f2 = destruct_flex_t' t2 in
  
negative.code:         t, wl
        end
      | _ ->
        failwith (BU.format3 "ensure_no_uvar_subst: expected a uvar at the head (%s-%s-%s)"
                             (Print.tag_of_term t0)
                             (Print.tag_of_term head)
                             (Print.tag_of_term (SS.compress head)))
  
  (* Only call if ensure_no_uvar_subst was called on t before *)
  let destruct_flex_t' t : flex_t =
  