Step * of Lemma per-class-base

[T:Type]. ∀[a:T]. ∀[b:per-class(T;a)].  (b a) supposing T ⊆Base
BY
((UnivCD THENA Auto) THEN (-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