---

Step * 1 of Lemma loc-on-path-nil


1. es : EO@i'
2. i : Id@i
3. (i ∈ [])@i
⊢ False
BY
{ Obvious }

---

Latex:



1.  es  :  EO@i'
2.  i  :  Id@i
3.  (i  \mmember{}  [])@i
\mvdash{}  False


By

Obvious

---

Home Index