anchor.diff:  let set (p:proofstate) : tac<unit> =
       mk_tac (fun _ -> Success ((), p))
   
  +let trysolve goal solution =
  +    Rel.teq_nosmt goal.context goal.witness solution
  +
   let solve goal solution =
  -    if Rel.teq_nosmt goal.context goal.witness solution
  +    if trysolve goal solution
       then ()
       else raise (TacFailure(BU.format3 "%s does not solve %s : %s"
                             (Print.term_to_string solution)
  
positive.code:         else let env' = Env.push_binders goal.context [b] in
               let typ' = comp_to_typ c in
               bind (new_uvar env' typ') (fun u ->
               if Rel.teq_nosmt goal.context goal.witness (U.abs [b] u None)
               then bind (replace_cur ({ goal with context = env';
                                                   goal_ty = bnorm env' typ';
                                                   witness = bnorm env' u})) (fun _ ->
  
negative.code:              let lbs, body = SS.close_let_rec [lb] body in
               let tm = mk (Tm_let ((true, lbs), body)) None goal.witness.pos in
               BU.print_string "calling teq_nosmt\n";
               let res = trysolve goal tm in
               if res
               then bind (replace_cur ({ goal with context = env';
                                                   goal_ty = bnorm env' (comp_to_typ c);
  