---

Step * of Lemma eclass3-total

∀[Info,B,C:Type]. ∀[X:EClass(B ─→ C)]. ∀[Y:EClass(B)]. ∀[es:EO+(Info)].
  (es-total-class(es;eclass3(X;Y))) supposing (es-total-class(es;X) and es-total-class(es;Y))
BY
{ (Auto
   THEN All(Unfold `es-total-class`)
   THEN Auto
   THEN All(\i.(InstHyp [⌈e⌉] i⋅ THENA CpltAuto))⋅
   THEN All(Unfold `class-ap`)
   THEN All(\i.(RWO "member-eclass-iff-size1<" i THENA Auto))⋅
   THEN BLemma `eclass3-member`
   THEN Auto) }

---

Latex:


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


By

(Auto
  THEN  All(Unfold  `es-total-class`)
  THEN  Auto
  THEN  All(\mbackslash{}i.(InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  i\mcdot{}  THENA  CpltAuto))\mcdot{}
  THEN  All(Unfold  `class-ap`)
  THEN  All(\mbackslash{}i.(RWO  "member-eclass-iff-size1<"  i  THENA  Auto))\mcdot{}
  THEN  BLemma  `eclass3-member`
  THEN  Auto)

---

Home Index