Rewrite the expression
The unification is performed using the transparency mode in
tt, then fallback to first-order unification,
and approximate context during unification.
cfg.new_goals specifies which unassigned metavariables become new goals,
and their order.
tt, then use type class resolution to instantiate
cfg.opt_param are ignored by this tactic
It a triple
(new_e, prf, metas) where
prf : e = new_e, and
is a list of all introduced meta variables,
even the assigned ones.
TODO(Leo): improve documentation and explain symm/occs