anchor.diff:      | [] -> fail "No more goals (1)"
       | hd::tl -> ret hd)
   
  -let add_irrelevant_goal (env:env) (phi:typ) : tac<unit> =
  -    bind cur_goal (fun cur ->
  +let add_irrelevant_goal (env:env) (phi:typ) opts : tac<unit> =
       let typ = U.mk_squash phi in
       bind (new_uvar env typ) (fun (u, g_u) ->
  -    let goal = { context = env; witness = u; goal_ty = typ; opts = cur.opts } in
  -    add_goals [goal]))
  +    let goal = { context = env; witness = u; goal_ty = typ; opts = opts } in
  +    add_goals [goal])
   
   let smt : tac<unit> =
       bind cur_goal (fun g ->
  
positive.code:  * calls apply_lemma to fully instantiate `u` and provide a proof of the equality.
   * If all that is successful, the term is rewritten.
   *)
  let pointwise_rec (ps : proofstate) (tau : tac<unit>) (env : Env.env) (t : term) : tac<term> =
      let t, lcomp, g = TcTerm.tc_term env t in
      if not (U.is_total_lcomp lcomp) || not (Rel.is_trivial g) then
          ret t // Don't do anything for possibly impure terms
  
negative.code:                     | _ -> failwith "exact_lemma: impossible: not a lemma"
      in
      if Rel.teq_nosmt goal.context post goal.goal_ty
      then let _ = solve goal t in bind dismiss (fun _ -> add_irrelevant_goal goal.context pre goal.opts)
      else fail3 "%s : %s does not exactly solve the goal %s"
                      (Print.term_to_string t)
                      (Print.term_to_string post)
  