---

Step * of Lemma pscm-type-at

∀s,A,I,alpha:Top.  ((A)s(alpha) ~ A((s)alpha))
BY
{ xxx((UnivCD THENA Auto) THEN RW  (SubC (SymbCompC [] 100)) 0 THEN EqCD)xxx }

---

Latex:

---

Latex:
\mforall{}s,A,I,alpha:Top.    ((A)s(alpha)  \msim{}  A((s)alpha))


By

---

Latex:
xxx((UnivCD  THENA  Auto)  THEN  RW    (SubC  (SymbCompC  []  100))  0  THEN  EqCD)xxx

---

Home Index