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.