---

Step * of Lemma es-interface-buffer_wf

∀[Info,A1:Type]. ∀[n:ℕ]. ∀[X:EClass(A1)].  (Buffer(n;X) ∈ EClass(A1 List))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[Info,A1:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[X:EClass(A1)].    (Buffer(n;X)  \mmember{}  EClass(A1  List))


By

---

Latex:
ProveWfLemma

---

Home Index