rfl
tactic extension for reflexive relations #
This extends the rfl
tactic so that it works on any reflexive relation,
provided the reflexivity lemma has been marked as @[refl]
.
Environment extensions for refl
lemmas