Commit 2023-06-05 07:16 92878218

fix: rewrites doesn't fail when trying an unimported lemma (#4537) Because of the global DiscrTree cache, rewrites was encountering lemmas that were not yet imported, and failing when calling mkConst. We also switch to using MVarId.rfl rather than MVarId.refl to see if goals can be closed, make sure that if a solution closes the goal it is reported ahead of other solutions, and slightly tweak the sort order again.