anchor.diff:                              (tts (goal_env goal) (U.mk_squash U_zero post))
                               (tts (goal_env goal) (goal_type goal))
       else
  -        bind (add_implicits implicits.implicits) (fun _ ->
           // We solve with (), we don't care about the witness if applying a lemma
           bind (solve' goal U.exp_unit) (fun _ ->
           let is_free_uvar uv t =
  
positive.code:     match lemma_or_sq comp with
      | None -> fail "not a lemma or squashed function"
      | Some (pre, post) ->
      let uvs, implicits, subst =
         List.fold_left (fun (uvs, guard, subst) (b, aq) ->
                 let b_t = SS.subst subst b.sort in
                 if is_unit_t b_t
                 then
                     // Simplification: if the argument is simply unit, then don't ask for it
                     (U.exp_unit, aq)::uvs, guard, S.NT(b, U.exp_unit)::subst
                 else
                     let u, _, g_u = TcUtil.new_implicit_var "apply_lemma" (goal_type goal).pos (goal_env goal) b_t in
                     (u, aq)::uvs,
                     Env.conj_guard guard g_u,
                     S.NT(b, u)::subst
                 )
         ([], guard, [])
         bs
      in
      let uvs = List.rev uvs in
      let pre  = SS.subst subst pre in
      let post = SS.subst subst post in
  
negative.code:     else
          None
  
  let rec fold_left (f : ('a -> 'b -> tac<'b>)) (e : 'b) (xs : list<'a>) : tac<'b> =
      match xs with
      | [] -> ret e
      | x::xs -> bind (f x e) (fun e' -> fold_left f e' xs)
  
  let apply_lemma (tm:term) : tac<unit> = wrap_err "apply_lemma" <| focus (
      bind get (fun ps ->
      mlog (fun () -> BU.print1 "apply_lemma: tm = %s\n" (Print.term_to_string tm)) (fun _ ->
  