This extends the
rfl tactic so that it works on any reflexive relation,
provided the reflexivity lemma has been marked as
MetaM version of the
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].
- One or more equations did not get rendered due to their size.