---

Step * 2 of Lemma loc-on-path-cons


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

---

Latex:



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


By

(RepUR  ``loc-on-path``  (0)  THEN  RWO  "member\_singleton"  (0)  THEN  Auto)\mcdot{}

---

Home Index