Try to close main goal by using equalities implied by the congruence closure module.
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 smt_tactic.add_lemmas.
The current set of lemmas can be retrieved using the tactic smt_tactic.get_lemmas.
Try the given tactic, and do nothing if it fails.
Keep applying the given tactic until it fails.
Apply the given tactic to all remaining goals.
Simplify the target type of the main goal.
Keep applying heuristic instantiation until the current goal is solved, or it fails.
Keep applying heuristic instantiation using the given lemmas until the current goal is solved, or it fails.