---

Step * of Lemma es-interface-vals-since_wf

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:EClass(T)]. ∀[Z:EClass(Top)]. ∀[e:E].  (X(Z',e] ∈ T List)
BY
{ Auto }

1
1. Info : Type
2. es : EO+(Info)
3. T : Type
4. X : EClass(T)
5. Z : EClass(Top)
6. e : E
⊢ X(Z',e] ∈ T List

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[Z:EClass(Top)].  \mforall{}[e:E].
    (X(Z',e]  \mmember{}  T  List)


By

---

Latex:
Auto

---

Home Index