rfl tactic extension for reflexive relations #
This extends the rfl tactic so that it works on reflexive relations other than =,
provided the reflexivity lemma has been marked as @[refl].
Equations
- One or more equations did not get rendered due to their size.