---

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


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

---

Latex:



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


By

(EqTypeCD  THEN  Auto)

---

Home Index