---

Step * 1 1 2 2 of Lemma global-eo-first

.....wf..... 
1. L : (Id × Top) List
2. e : {e:ℕ||L||| True} 
3. first(e) = (∀x∈upto(e).¬bloc(x) = loc(e))_b
4. z : 𝔹
⊢ first(e) ~ z ∈ Type
BY
{ (GenConcl ⌜first(e) = x⌝⋅ THENA Auto) }

1
1. L : (Id × Top) List
2. e : {e:ℕ||L||| True} 
3. first(e) = (∀x∈upto(e).¬bloc(x) = loc(e))_b
4. z : 𝔹
5. x : 𝔹@i
6. first(e) = x@i
⊢ x ~ z ∈ Type

---

Latex:

---

Latex:
.....wf..... 
1.  L  :  (Id  \mtimes{}  Top)  List
2.  e  :  \{e:\mBbbN{}||L|||  True\} 
3.  first(e)  =  (\mforall{}x\mmember{}upto(e).\mneg{}\msubb{}loc(x)  =  loc(e))\_b
4.  z  :  \mBbbB{}
\mvdash{}  first(e)  \msim{}  z  \mmember{}  Type


By

---

Latex:
(GenConcl  \mkleeneopen{}first(e)  =  x\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index