---

Step * of Lemma global-eo-first

∀[L:(Id × Top) List]. ∀[e:E].  (first(e) ~ (∀x∈upto(e).¬bloc(x) = loc(e))_b)
BY
{ Intros }

1
1. [L] : (Id × Top) List
2. [e] : E
⊢ first(e) ~ (∀x∈upto(e).¬bloc(x) = loc(e))_b

---

Latex:

---

Latex:
\mforall{}[L:(Id  \mtimes{}  Top)  List].  \mforall{}[e:E].    (first(e)  \msim{}  (\mforall{}x\mmember{}upto(e).\mneg{}\msubb{}loc(x)  =  loc(e))\_b)


By

---

Latex:
Intros

---

Home Index