---

Step * of Lemma loc-on-path-cons

∀es:EO. ∀L:E List. ∀e:E. ∀i:Id.  (loc-on-path(es;i;[e / L]) ⇐⇒ (loc(e) = i ∈ Id) ∨ loc-on-path(es;i;L))
BY
{ ((UnivCD THENA Auto)
   THEN Subst' [e / L] ~ [e] @ L 0
   THEN Try (Complete ((Reduce 0 THEN Auto)))
   THEN (RWO "loc-on-path-append" 0 THEN Auto)
   THEN ParallelLast) }

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

2
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])

---

Latex:


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


By

((UnivCD  THENA  Auto)
  THEN  Subst'  [e  /  L]  \msim{}  [e]  @  L  0
  THEN  Try  (Complete  ((Reduce  0  THEN  Auto)))
  THEN  (RWO  "loc-on-path-append"  0  THEN  Auto)
  THEN  ParallelLast)

---

Home Index