---

Step * of Lemma ranked-eo-info-le-before

∀[L:Id ─→ (Top List)]. ∀[rk:Top]. ∀[e:E].  (map(λe.info(e);≤loc(e)) ~ firstn((snd(e)) + 1;L (fst(e))))
BY
{ (Intros THEN RWW "ranked-eo-E-sq" 0 THEN Auto) }

1
1. [L] : Id ─→ (Top List)
2. [rk] : Top
3. [e] : E
⊢ map(λe.info(e);≤loc(e)) ~ firstn((snd(e)) + 1;L (fst(e)))

---

Latex:

---

Latex:
\mforall{}[L:Id  {}\mrightarrow{}  (Top  List)].  \mforall{}[rk:Top].  \mforall{}[e:E].
    (map(\mlambda{}e.info(e);\mleq{}loc(e))  \msim{}  firstn((snd(e))  +  1;L  (fst(e))))


By

---

Latex:
(Intros  THEN  RWW  "ranked-eo-E-sq"  0  THEN  Auto)

---

Home Index