---

Step * of Lemma eclass3-single-val

∀[Info,B,C:Type]. ∀[X:EClass(B ─→ C)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)].
  (single-valued-classrel(es;eclass3(X;Y);C)) supposing 
     (single-valued-classrel(es;X;B ─→ C) and 
     single-valued-classrel(es;Y;B))
BY
{ ((UnivCD THENA Auto)
   THEN UnfoldTopAb 0
   THEN Auto
   THEN All MaUseClassRel
   THEN (SimpleSubstTerm ⌈v1⌉ 0⋅ THENA Auto)
   THEN (SimpleSubstTerm ⌈v2⌉ 0⋅ THENA Auto)
   THEN RepeatFor 2 (UseSingleVal (-8) (-3))
   THEN Auto) }

---

Latex:


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


By

((UnivCD  THENA  Auto)
  THEN  UnfoldTopAb  0
  THEN  Auto
  THEN  All  MaUseClassRel
  THEN  (SimpleSubstTerm  \mkleeneopen{}v1\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (SimpleSubstTerm  \mkleeneopen{}v2\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (UseSingleVal  (-8)  (-3))
  THEN  Auto)

---

Home Index