---

Step * of Lemma simple-comb-es-sv

∀[Info,B:Type]. ∀[n:ℕ]. ∀[A:ℕn ─→ Type]. ∀[Xs:k:ℕn ─→ EClass(A k)]. ∀[F:(k:ℕn ─→ bag(A k)) ─→ bag(B)]. ∀[es:EO+(Info)].
  (es-sv-class(es;simple-comb(F;Xs))) supposing 
     ((∀bs:k:ℕn ─→ bag(A k). ((∀k:ℕn. (#(bs k) ≤ 1)) ⇒ (#(F bs) ≤ 1))) and 
     (∀k:ℕn. es-sv-class(es;Xs k)))
BY
{ ((UnivCD THENA MaAuto) THEN RepUR ``es-sv-class simple-comb`` 0 THEN Auto THEN BHyp (-2)  THEN Reduce 0 THEN MaAuto) }

---

Latex:

---

Latex:
\mforall{}[Info,B:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[Xs:k:\mBbbN{}n  {}\mrightarrow{}  EClass(A  k)].
\mforall{}[F:(k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k))  {}\mrightarrow{}  bag(B)].  \mforall{}[es:EO+(Info)].
    (es-sv-class(es;simple-comb(F;Xs)))  supposing 
          ((\mforall{}bs:k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k).  ((\mforall{}k:\mBbbN{}n.  (\#(bs  k)  \mleq{}  1))  {}\mRightarrow{}  (\#(F  bs)  \mleq{}  1)))  and 
          (\mforall{}k:\mBbbN{}n.  es-sv-class(es;Xs  k)))


By

---

Latex:
((UnivCD  THENA  MaAuto)
  THEN  RepUR  ``es-sv-class  simple-comb``  0
  THEN  Auto
  THEN  BHyp  (-2) 
  THEN  Reduce  0
  THEN  MaAuto)

---

Home Index