anchor.diff:   * 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 pointwise_rec (ps : proofstate) (tau : tac<unit>) opts (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
  
positive.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)
      else fail3 "%s : %s does not exactly solve the goal %s"
                      (Print.term_to_string t)
                      (Print.term_to_string post)
  
negative.code:         log ps (fun () ->
              BU.print2 "Pointwise_rec: making equality %s = %s\n" (Print.term_to_string t)
                                                                   (Print.term_to_string ut));
          bind (add_irrelevant_goal env (U.mk_eq2 (TcTerm.universe_of env typ) typ t ut) opts) (fun _ ->
          focus (
              bind tau (fun _ ->
              Rel.force_trivial_guard env guard;
  