---

Step * of Lemma cond-class-subtype1

∀[Info,A:Type]. ∀[X,Y:EClass(A)]. ∀[es:EO+(Info)].  (E(X) ⊆r E([X?Y]))
BY
{ (Auto THEN D 0 THEN Auto THEN D -1 THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. Info : Type
2. A : Type
3. X : EClass(A)
4. Y : EClass(A)
5. es : EO+(Info)
6. x : E@i
7. ↑x ∈b X@i
⊢ ↑x ∈b [X?Y]

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[X,Y:EClass(A)].  \mforall{}[es:EO+(Info)].    (E(X)  \msubseteq{}r  E([X?Y]))


By

(Auto  THEN  D  0  THEN  Auto  THEN  D  -1  THEN  MemTypeCD  THEN  Auto)

---

Home Index