---

Step * of Lemma swap_cons

No Annotations
∀[T:Type]. ∀[L:T List]. ∀[x:T]. ∀[i,j:ℕ+||L|| + 1].  (swap([x / L];i;j) = [x / swap(L;i - 1;j - 1)] ∈ (T List))
BY
{ (((Auto THEN BackThruLemma `list_extensionality`) THEN Reduce 0) THEN Auto') }

1
1. T : Type
2. L : T List
3. x : T
4. i : ℕ+||L|| + 1
5. j : ℕ+||L|| + 1
6. i1 : ℕ
7. i1 < ||swap([x / L];i;j)||
⊢ swap([x / L];i;j)[i1] = [x / swap(L;i - 1;j - 1)][i1] ∈ T

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[x:T].  \mforall{}[i,j:\mBbbN{}\msupplus{}||L||  +  1].    (swap([x  /  L];i;j)  =  [x  /  swap(L;i  -  1;j  -  1)])


By

---

Latex:
(((Auto  THEN  BackThruLemma  `list\_extensionality`)  THEN  Reduce  0)  THEN  Auto')

---

Home Index