---

Step * 1 of Lemma classfun_wf


1. Info : Type
2. T : Type
3. es : EO+(Info)
4. X : EClass(T)
5. e : E
6. 1 ≤ #(X(e))
7. single-valued-bag(X es e;T)
⊢ 0 < #(X es e)
BY
{ (Fold `class-ap` 0 THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  T  :  Type
3.  es  :  EO+(Info)
4.  X  :  EClass(T)
5.  e  :  E
6.  1  \mleq{}  \#(X(e))
7.  single-valued-bag(X  es  e;T)
\mvdash{}  0  <  \#(X  es  e)


By

(Fold  `class-ap`  0  THEN  Auto)

---

Home Index