---

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

∀L:Top List. ∀i:Id. ∀e:E.  (map(λe.info(e);≤loc(e)) ~ firstn(e + 1;L))
BY
{ Intros }

1
1. L : Top List@i
2. i : Id@i
3. e : E@i
⊢ map(λe.info(e);≤loc(e)) ~ firstn(e + 1;L)

2
1. L : Top List@i
2. i : Id@i
⊢ E = E ∈ Type

---

Latex:

---

Latex:
\mforall{}L:Top  List.  \mforall{}i:Id.  \mforall{}e:E.    (map(\mlambda{}e.info(e);\mleq{}loc(e))  \msim{}  firstn(e  +  1;L))


By

---

Latex:
Intros

---

Home Index