Lean.MVarId.liftReflToEq
#
Convert a goal of the form x ~ y
into the form x = y
, where ~
is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl]
.
If this can't be done, returns the original MVarId
.
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].