---

Step * of Lemma es-blocl_wf

∀[es:EO]. ∀[e1,e2:E].  (es-blocl(es;e1;e2) ∈ 𝔹)
BY
{ ProveWfLemma }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e1,e2:E].    (es-blocl(es;e1;e2)  \mmember{}  \mBbbB{})


By

ProveWfLemma

---

Home Index