Produce new facts using heuristic lemma instantiation based on E-matching.
This tactic tries to match patterns from lemmas in the main goal with terms
in the main goal. The set of lemmas is populated with theorems
tagged with the attribute specified at smt_config.em_attr, and lemmas
added using tactics such as
The current set of lemmas can be retrieved using the tactic
Simplify the target type of the main goal.