---

Step * of Lemma select_cons_tl_sq2

∀[i:ℕ]. ∀[x,l:Top].  ([x / l][i + 1] ~ l[i])
BY
{ ((UnivCD THENA Auto) THEN RWO "select-cons-tl" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[i:\mBbbN{}].  \mforall{}[x,l:Top].    ([x  /  l][i  +  1]  \msim{}  l[i])


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "select-cons-tl"  0  THEN  Auto)

---

Home Index