Step
*
1
2
1
of Lemma
es-interval-eq
1. es : EO
2. e : E
3. v : E List@i
⊢ (v = [] ∈ (E List)) 
⇒ (v ~ [])
BY
{ D (-1) }
1
1. es : EO
2. e : E
⊢ ([] = [] ∈ (E List)) 
⇒ ([] ~ [])
2
1. es : EO
2. e : E
3. u : E
4. v : E List
⊢ ([u / v] = [] ∈ (E List)) 
⇒ ([u / v] ~ [])
Latex:
1.  es  :  EO
2.  e  :  E
3.  v  :  E  List@i
\mvdash{}  (v  =  [])  {}\mRightarrow{}  (v  \msim{}  [])
By
D  (-1)
Home
Index