---

Step * of Lemma loc-on-path-singleton

∀es:EO. ∀e:E. ∀i:Id.  (loc-on-path(es;i;[e]) ⇐⇒ loc(e) = i ∈ Id)
BY
{ ((UnivCD THENA Auto) THEN RWO "loc-on-path-cons" 0 THEN Auto) }

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

---

Latex:


\mforall{}es:EO.  \mforall{}e:E.  \mforall{}i:Id.    (loc-on-path(es;i;[e])  \mLeftarrow{}{}\mRightarrow{}  loc(e)  =  i)


By

((UnivCD  THENA  Auto)  THEN  RWO  "loc-on-path-cons"  0  THEN  Auto)

---

Home Index