Step
*
of Lemma
ext-eq-equiv
EquivRel(Type;A,B.A ≡ B)
BY
{ (RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto)) THEN RelRST THEN Auto) }
Latex:
Latex:
EquivRel(Type;A,B.A  \mequiv{}  B)
By
Latex:
(RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto))  THEN  RelRST  THEN  Auto)
Home
Index