---

Step * of Lemma equiv-substs-equiv-rel

No Annotations
∀[opr:Type]. EquivRel((varname() × term(opr)) List;s1,s2.equiv-substs(opr;s1;s2))
BY
{ (InstLemma `alpha-eq-equiv-rel` []
   THEN RepeatFor 2 (ParallelLast')
   THEN RepeatFor 2 (D -1)
   THEN RepeatFor 2 ((D 0 THEN Auto))
   THEN All (RepUR ``equiv-substs``)
   THEN Try (ParallelLast)
   THEN Auto
   THEN D 9 With ⌜x⌝ 
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  EquivRel((varname()  \mtimes{}  term(opr))  List;s1,s2.equiv-substs(opr;s1;s2))


By

---

Latex:
(InstLemma  `alpha-eq-equiv-rel`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  RepeatFor  2  (D  -1)
  THEN  RepeatFor  2  ((D  0  THEN  Auto))
  THEN  All  (RepUR  ``equiv-substs``)
  THEN  Try  (ParallelLast)
  THEN  Auto
  THEN  D  9  With  \mkleeneopen{}x\mkleeneclose{} 
  THEN  Auto)

---

Home Index