anchor.diff:      | _ -> failwith "Not a flex-uvar"
   
   (* Make sure the uvar at the head of t0 is not affected by a
  - * substitution.
  + * 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 unchanged (the changes only happen in the UF graph).
  + * without a substitution. This function returns t again, though it is
  + * unchanged (the changes only happen in the UF graph).
    *
  - * The way we generate the new uvar is find the x's in the domain of ?u
  - * that are not affected by the substitution and make a new variable with
  - * only those binders in the domain. The ones that are affected we will
  - * "hoist" by making the type of ?u' an arrow.
  + * The way we generate the new uvar is by making a new variable with
  + * that is "hoisted" and which we apply to the binders of the original
  + * uvar. There is an optimization in place to hoist as few binders as
  + * possible.
    *
  - * Example:
  - * If we have (x,y |- ?u : ty)[(x:a) <- x, (y:int) <- 42], we will make
  - * ?u' with x in its binders, abstracted over y:
  + * Example: If we have ((x:a),(y:b),(z:c) |- ?u : ty)[y <- 42], we will
  + * make ?u' with x in its binders, abstracted over y and z:
    *
  - * (x |- ?u') : int -> ty
  + * (x |- ?u') : b -> c -> ty
    *
  - * and then solve
  + * (we keep x since it's unaffected by the substitution; z is not since
  + * it has y in scope) and then solve
    *
  - * ?u <- (?u' y)
  + * ?u <- (?u' y z)
    *
  - * Which means the original term now compresses to ?u' 42. The flex
  + * Which means the original term now compresses to ?u' 42 z. The flex
    * problem we now return is
    *
  - * ?u', [42]
  + * ?u', [42 z]
    *
  - * We return early if the substitution is empty or if the uvar is
  + * We also return early if the substitution is empty or if the uvar is
    * totally unaffected by it.
  - *
  - * (It's not strictly needed for this function to return t, compressing
  - *  t0 will give you the same term.)
    *)
   let ensure_no_uvar_subst (t0:term) (wl:worklist)
     : term * worklist
     = (* Returns true iff the variable x is not affected by substitution s *)
  -    let not_affected_by (s:subst_ts) (x:bv) : bool =
  +    let bv_not_affected_by (s:subst_ts) (x:bv) : bool =
         let t_x = S.bv_to_name x in
         let t_x' = SS.subst' s t_x in
         match (SS.compress t_x').n with
  
positive.code:       | Tm_app({n=Tm_uvar _}, _), Tm_uvar _
        | Tm_uvar _,                Tm_app({n=Tm_uvar _}, _)
        | Tm_app({n=Tm_uvar _}, _), Tm_app({n=Tm_uvar _}, _) ->
          (* We need to do both ensure_no_uvar_subst calls before
           * destructing since we might have the same uvar on
           * both sides. See #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
  
negative.code:         t, wl
        end
      | _ ->
        failwith "ensure_no_uvar_subst: expected a uvar at the head"
  
  (* Only call if ensure_no_uvar_subst was called on t before *)
  let destruct_flex_t' t : flex_t =
  