anchor.diff:  let trivial : tac<unit> =
       bind cur_goal (fun goal ->
       if istrivial goal.context goal.goal_ty
  -    then (solve goal U.exp_unit; dismiss)
  +    then solve goal U.exp_unit
       else fail1 "Not a trivial goal: %s" (N.term_to_string goal.context goal.goal_ty)
       )
   
  
positive.code:                     | _ -> failwith "exact_lemma: impossible: not a lemma"
      in
      if do_unify 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"
                      (N.term_to_string goal.context t)
                      (N.term_to_string goal.context post)
  
negative.code:         | Tm_fvar fv, [_; (l, _); (r, _)] when S.fv_eq_lid fv PC.eq2_lid ->
              if not (do_unify g.context l r)
              then fail2 "trefl: not a trivial equality (%s vs %s)" (N.term_to_string g.context l) (N.term_to_string g.context r)
              else solve g U.exp_unit
          | hd, _ ->
              fail1 "trefl: not an equality (%s)" (N.term_to_string g.context t)
          end
  