---

Step * 1 2 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 < ||[x / L]||
8. ¬(i1 = 0 ∈ ℤ)
⊢ [x / L][(i, j) i1] = L[(i - 1, j - 1) (i1 - 1)] ∈ T
BY
{ (Subst' ((i, j) i1) = (((i - 1, j - 1) (i1 - 1)) + 1) ∈ ℤ 0⋅
   THEN Try (Complete ((Unfold `flip` 0 THEN Reduce 0 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  <  ||[x  /  L]||
8.  \mneg{}(i1  =  0)
\mvdash{}  [x  /  L][(i,  j)  i1]  =  L[(i  -  1,  j  -  1)  (i1  -  1)]


By

---

Latex:
(Subst'  ((i,  j)  i1)  =  (((i  -  1,  j  -  1)  (i1  -  1))  +  1)  0\mcdot{}
  THEN  Try  (Complete  ((Unfold  `flip`  0  THEN  Reduce  0  THEN  Auto')))
  )

---

Home Index