---

Step * of Lemma swap_length

∀[T:Type]. ∀[L:T List]. ∀[i,j:ℕ||L||].  (||swap(L;i;j)|| = ||L|| ∈ ℤ)
BY
{ (Unfold `swap` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[i,j:\mBbbN{}||L||].    (||swap(L;i;j)||  =  ||L||)


By

---

Latex:
(Unfold  `swap`  0  THEN  Auto)

---

Home Index