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].
This tactic applies to a goal whose target has the form x ~ x, where ~ is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
Equations
- One or more equations did not get rendered due to their size.