---

Step * of Lemma per-class-base

∀[T:Type]. ∀[a:T]. ∀[b:per-class(T;a)].  (b ~ a) supposing T ⊆r Base
BY
{ ((UnivCD THENA Auto) THEN D (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[a:T].  \mforall{}[b:per-class(T;a)].    (b  \msim{}  a)  supposing  T  \msubseteq{}r  Base


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  (-1)  THEN  Auto)

---

Home Index