---

Step * of Lemma select_cons_tl_sq

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

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].  \mforall{}[l:T  List].  \mforall{}[i:\mBbbN{}||l||].    ([x  /  l][i  +  1]  \msim{}  l[i])


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "select-cons-tl"  0\mcdot{}  THEN  Auto)

---

Home Index