---

Step * 2 1 of Lemma null-es-hist


1. Info : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. loc(e2) = loc(e1) ∈ Id
6. ¬(e2 <loc e1)
7. ↑null([e1, e2])@i
⊢ (e2 <loc e1)
BY
{ ((RW assert_pushdownC (-1)) THENA Auto) }

1
1. Info : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
5. loc(e2) = loc(e1) ∈ Id
6. ¬(e2 <loc e1)
7. [e1, e2] = [] ∈ (E List)
⊢ (e2 <loc e1)

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  e1  :  E@i
4.  e2  :  E@i
5.  loc(e2)  =  loc(e1)
6.  \mneg{}(e2  <loc  e1)
7.  \muparrow{}null([e1,  e2])@i
\mvdash{}  (e2  <loc  e1)


By

((RW  assert\_pushdownC  (-1))  THENA  Auto)

---

Home Index