---

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


1. es : EO@i'
2. e : E@i
3. i : Id@i
4. loc-on-path(es;i;[])@i
⊢ loc(e) = i ∈ Id
BY
{ (RWO "loc-on-path-nil" (-1)⋅ THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  i  :  Id@i
4.  loc-on-path(es;i;[])@i
\mvdash{}  loc(e)  =  i


By

(RWO  "loc-on-path-nil"  (-1)\mcdot{}  THEN  Auto)

---

Home Index