---

Step * of Lemma eclass1-single-val

∀[Info,B,C:Type]. ∀[X:EClass(B)]. ∀[f:Id ─→ B ─→ C]. ∀[es:EO+(Info)].
  single-valued-classrel(es;(f o X);C) supposing single-valued-classrel(es;X;B)
BY
{ ((UnivCD THENA Auto) THEN UnfoldTopAb 0 THEN Auto THEN All(MaUseClassRel) THEN SingleVal `e' THEN Auto) }

---

Latex:


\mforall{}[Info,B,C:Type].  \mforall{}[X:EClass(B)].  \mforall{}[f:Id  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[es:EO+(Info)].
    single-valued-classrel(es;(f  o  X);C)  supposing  single-valued-classrel(es;X;B)


By

((UnivCD  THENA  Auto)
  THEN  UnfoldTopAb  0
  THEN  Auto
  THEN  All(MaUseClassRel)
  THEN  SingleVal  `e'
  THEN  Auto)

---

Home Index