anchor.diff:      | Inr r -> ret r
       | Inl _ -> fail e)))) // keep original error
   
  -let uvar_free_in_goal (u:uvar) (g:goal) =
  -    if g.is_guard then false else
  -    let free_uvars = List.map (fun u -> u.ctx_uvar_head) (BU.set_elements (SF.uvars (goal_type g))) in
  -    List.existsML (UF.equiv u) free_uvars
  -
  -let uvar_free (u:uvar) (ps:proofstate) : bool =
  -    List.existsML (uvar_free_in_goal u) ps.goals
  -
   let rec mapM (f : 'a -> tac<'b>) (l : list<'a>) : tac<list<'b>> =
       match l with
       | [] -> ret []
  
positive.code:         bind (mapM f xs) (fun ys ->
          ret (y::ys)))
  
  exception NoUnif
  
  // uopt: Don't add goals for implicits that appear free in posterior goals.
  // This is very handy for users, allowing to turn
  
negative.code: // |- a = ?u
  // |- ?u = c
  //
  // without asking for |- ?u : Type first, which will most likely be instantiated when
  // solving any of these two goals. In any case, if ?u is not solved, we will later fail.
  // TODO: this should probably be made into a user tactic
  let apply (uopt:bool) (tm:term) : tac<unit> = wrap_err "apply" <|
      mlog (fun () -> BU.print1 "apply: tm = %s\n" (Print.term_to_string tm)) (fun _ ->
      bind (cur_goal ()) (fun goal ->
      let e = goal_env goal in
      bind (__tc e tm) (fun (tm, typ, guard) ->
      // Focus helps keep the goal order
      let typ = bnorm e typ in
      bind (try_match_by_application e typ (goal_type goal)) (fun uvs ->
      let w = List.fold_right (fun (uvt, q, _) w -> U.mk_app w [(uvt, q)]) uvs tm in
  
      let uvset = List.fold_right (fun (_, _, uv) s -> BU.set_union s (SF.uvars uv.ctx_uvar_typ)) uvs (SF.new_uv_set ()) in
      let free_in_some_goal uv =
          BU.set_mem uv uvset
      in
      bind (solve' goal w) (fun () ->
      bind (mapM (fun (uvt, q, uv) ->
                   match UF.find uv.ctx_uvar_head with
                   (* Already (at least partially) solved, skip asking the user for it *)
                   | Some _ ->
                         ret ()
                   (* Not instantiated at all *)
                   | None ->
                      (* We might still not add it if uopt is on, as described above *)
                      if uopt && free_in_some_goal uv
                      then ret ()
                      else add_goals [bnorm_goal ({ goal with
                                                    goal_ctx_uvar = uv;
                                                    is_guard = false; })]
                 ) uvs) (fun _ ->
      proc_guard "apply guard" e guard
      ))))))
  
  // returns pre and post
  let lemma_or_sq (c : comp) : option<(term * term)> =
  