---

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


1. L : Top List@i
2. i : Id@i
⊢ E = E ∈ Type
BY
{ (RWO "list-eo-E-sq" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  L  :  Top  List@i
2.  i  :  Id@i
\mvdash{}  E  =  E


By

---

Latex:
(RWO  "list-eo-E-sq"  0  THEN  Auto)

---

Home Index