---

Step * 1 1 1 1 of Lemma swap_cons


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)||
8. i1 = 0 ∈ ℤ
⊢ [x / L][(i, j) 0] = x ∈ T
BY
{ (((((Subst' ((i, j) 0) = 0 ∈ ℤ 0 THEN Reduce 0) THEN Auto) THEN Unfold `flip` 0) THEN Reduce 0)
   THEN Repeat (SplitOnConclITE THEN Auto')
   ) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  x  :  T
4.  i  :  \mBbbN{}\msupplus{}||L||  +  1
5.  j  :  \mBbbN{}\msupplus{}||L||  +  1
6.  i1  :  \mBbbN{}
7.  i1  <  ||swap([x  /  L];i;j)||
8.  i1  =  0
\mvdash{}  [x  /  L][(i,  j)  0]  =  x


By

---

Latex:
(((((Subst'  ((i,  j)  0)  =  0  0  THEN  Reduce  0)  THEN  Auto)  THEN  Unfold  `flip`  0)  THEN  Reduce  0)
  THEN  Repeat  (SplitOnConclITE  THEN  Auto')
  )

---

Home Index