anchor.diff:      bind cur_goal (fun goal ->
       if istrivial goal.context goal.goal_ty
       then solve goal U.exp_unit
  -    else fail1 "Not a trivial goal: %s" (N.term_to_string goal.context goal.goal_ty)
  +    else fail1 "Not a trivial goal: %s" (tts goal.context goal.goal_ty)
       )
   
   let add_goal_from_guard (reason:string) (e:env) (g : guard_t) opts : tac<unit> =
  
positive.code:     // Focus helps keep the goal order
      try_unif (focus (bind (__apply uopt tm typ) (fun _ -> add_goal_from_guard "apply guard" goal.context guard goal.opts)))
               (fail3 "Cannot instantiate %s (of type %s) to match goal (%s)"
                              (N.term_to_string goal.context tm)
                              (N.term_to_string goal.context typ)
                              (N.term_to_string goal.context goal.goal_ty))
      )))
  
  let apply_lemma (tm:term) : tac<unit> = wrap_err "apply_lemma" <| focus (
  
negative.code:     if is_irrelevant g then
          bind dismiss (fun _ -> add_smt_goals [g])
      else
          fail1 "goal is not irrelevant: cannot dispatch to smt (%s)" (tts g.context g.goal_ty)
      )
  
  let divide (n:Z.t) (l : tac<'a>) (r : tac<'b>) : tac<('a * 'b)> =
  