---

Step * of Lemma eclass-val_wf

∀[T:Type]. ∀[A:es:EO+(T) ─→ E ─→ Type]. ∀[X:EClass(A[es;e])]. ∀[eo:EO+(T)]. ∀[e:E].  X(e) ∈ A[eo;e] supposing ↑e ∈b X
BY
{ Auto }

1
1. T : Type
2. A : es:EO+(T) ─→ E ─→ Type
3. X : EClass(A[es;e])
4. eo : EO+(T)
5. e : E
6. ↑e ∈b X
⊢ X(e) ∈ A[eo;e]

---

Latex:


\mforall{}[T:Type].  \mforall{}[A:es:EO+(T)  {}\mrightarrow{}  E  {}\mrightarrow{}  Type].  \mforall{}[X:EClass(A[es;e])].  \mforall{}[eo:EO+(T)].  \mforall{}[e:E].
    X(e)  \mmember{}  A[eo;e]  supposing  \muparrow{}e  \mmember{}\msubb{}  X


By

Auto

---

Home Index