---

Step * of Lemma simple-comb-1-single-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[F:A ⟶ B]. ∀[X:EClass(A)].
  single-valued-classrel(es;lifting-1(F)|X|;B) supposing single-valued-classrel(es;X;A)
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``single-valued-classrel`` 0
   THEN Auto
   THEN MaUseClassRel (-2)
   THEN MaUseClassRel (-1)
   THEN UseSingleVal (-4) (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B:Type].  \mforall{}[F:A  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].
    single-valued-classrel(es;lifting-1(F)|X|;B)  supposing  single-valued-classrel(es;X;A)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``single-valued-classrel``  0
  THEN  Auto
  THEN  MaUseClassRel  (-2)
  THEN  MaUseClassRel  (-1)
  THEN  UseSingleVal  (-4)  (-1)
  THEN  Auto)

---

Home Index