---

Step * of Lemma es-interface-predecessors-sorted-by-le

∀[Info:Type]. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E.  sorted-by(λx,y. x ≤loc y ;≤(X)(e))
BY
{ (InstLemma `es-interface-predecessors-sorted-by-locl` [] THEN RepeatFor 4 (ParallelLast')) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. e : E@i
5. sorted-by(λx,y. (x <loc y);≤(X)(e))
⊢ sorted-by(λx,y. x ≤loc y ;≤(X)(e))

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}e:E.    sorted-by(\mlambda{}x,y.  x  \mleq{}loc  y  ;\mleq{}(X)(e))


By

---

Latex:
(InstLemma  `es-interface-predecessors-sorted-by-locl`  []  THEN  RepeatFor  4  (ParallelLast'))

---

Home Index