---

Step * of Lemma loc-on-path-nil

∀es:EO. ∀i:Id.  (loc-on-path(es;i;[]) ⇐⇒ False)
BY
{ (Auto THEN Unfold `loc-on-path` -1 THEN Reduce (-1)) }

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Unfold  `loc-on-path`  -1  THEN  Reduce  (-1))

---

Home Index