---

Step * of Lemma alpha-eq-equiv-rel

No Annotations
∀[opr:Type]. EquivRel(term(opr);a,b.alpha-eq-terms(opr;a;b))
BY
{ (Auto
   THEN RepeatFor 2 ((D 0 THEN Auto))
   THEN All (RepUR ``alpha-eq-terms``)
   THEN ((FLemma `alpha-aux-trans` [-1;-2] THEN Auto) ORELSE EAuto 1)) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  EquivRel(term(opr);a,b.alpha-eq-terms(opr;a;b))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  ((D  0  THEN  Auto))
  THEN  All  (RepUR  ``alpha-eq-terms``)
  THEN  ((FLemma  `alpha-aux-trans`  [-1;-2]  THEN  Auto)  ORELSE  EAuto  1))

---

Home Index