---

Step * of Lemma es-closed-open-interval-sorted-by

∀[Info:Type]. ∀es:EO+(Info). ∀e1,e2:E.  sorted-by(λx,y. (x <loc y);[e1;e2))
BY
{ (Auto THEN RepUR ``es-closed-open-interval`` 0 THEN (BLemma `sorted-by-filter` THENA Auto)) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. e1 : E@i
4. e2 : E@i
⊢ sorted-by(λx,y. (x <loc y);before(e2))

---

Latex:


\mforall{}[Info:Type].  \mforall{}es:EO+(Info).  \mforall{}e1,e2:E.    sorted-by(\mlambda{}x,y.  (x  <loc  y);[e1;e2))


By

(Auto  THEN  RepUR  ``es-closed-open-interval``  0  THEN  (BLemma  `sorted-by-filter`  THENA  Auto))

---

Home Index