1. es : EO
2. e : E
3. v : E List@i
⊢ (v = [] ∈ (E List))
(v ~ [])
{ D (-1) }
⊢ ([] = [] ∈ (E List))
([] ~ [])
3. u : E
4. v : E List
⊢ ([u / v] = [] ∈ (E List))
([u / v] ~ [])