---

Step * 1 of Lemma member-es-le-before3


1. es : EO@i'
2. e : E@i
3. e' : {e':E| e' ≤loc e } @i
4. i : ℕ@i
5. i < ||≤loc(e)||@i
6. e' = ≤loc(e)[i] ∈ {e':E| e' ≤loc e } @i
⊢ e' = ≤loc(e)[i] ∈ E
BY
{ (EqTypeHD (-1) THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  \{e':E|  e'  \mleq{}loc  e  \}  @i
4.  i  :  \mBbbN{}@i
5.  i  <  ||\mleq{}loc(e)||@i
6.  e'  =  \mleq{}loc(e)[i]@i
\mvdash{}  e'  =  \mleq{}loc(e)[i]


By

(EqTypeHD  (-1)  THEN  Auto)

---

Home Index