---

Step * 2 2 2 1 of Lemma cons_sublist_cons


1. T : Type
2. x1 : T
3. x2 : T
4. L1 : T List
5. L2 : T List
6. f : ℕ||L1|| + 1 ⟶ ℕ||L2||
7. increasing(f;||L1|| + 1)
8. ∀j:ℕ||L1|| + 1. ([x1 / L1][j] = L2[f j] ∈ T)
9. increasing(λj.((f j) + 1);||L1|| + 1)
10. j : ℕ||L1|| + 1
⊢ [x1 / L1][j] = [x2 / L2][(f j) + 1] ∈ T
BY
{ Subst [x2 / L2][(f j) + 1] = L2[f j] ∈ T 0 }

1
.....equality..... 
1. T : Type
2. x1 : T
3. x2 : T
4. L1 : T List
5. L2 : T List
6. f : ℕ||L1|| + 1 ⟶ ℕ||L2||
7. increasing(f;||L1|| + 1)
8. ∀j:ℕ||L1|| + 1. ([x1 / L1][j] = L2[f j] ∈ T)
9. increasing(λj.((f j) + 1);||L1|| + 1)
10. j : ℕ||L1|| + 1
⊢ [x2 / L2][(f j) + 1] = L2[f j] ∈ T

2
1. T : Type
2. x1 : T
3. x2 : T
4. L1 : T List
5. L2 : T List
6. f : ℕ||L1|| + 1 ⟶ ℕ||L2||
7. increasing(f;||L1|| + 1)
8. ∀j:ℕ||L1|| + 1. ([x1 / L1][j] = L2[f j] ∈ T)
9. increasing(λj.((f j) + 1);||L1|| + 1)
10. j : ℕ||L1|| + 1
⊢ [x1 / L1][j] = L2[f j] ∈ T

3
.....wf..... 
1. T : Type
2. x1 : T
3. x2 : T
4. L1 : T List
5. L2 : T List
6. f : ℕ||L1|| + 1 ⟶ ℕ||L2||
7. increasing(f;||L1|| + 1)
8. ∀j:ℕ||L1|| + 1. ([x1 / L1][j] = L2[f j] ∈ T)
9. increasing(λj.((f j) + 1);||L1|| + 1)
10. j : ℕ||L1|| + 1
11. z : T
⊢ [x1 / L1][j] = z ∈ T ∈ ℙ

---

Latex:

---

Latex:

1.  T  :  Type
2.  x1  :  T
3.  x2  :  T
4.  L1  :  T  List
5.  L2  :  T  List
6.  f  :  \mBbbN{}||L1||  +  1  {}\mrightarrow{}  \mBbbN{}||L2||
7.  increasing(f;||L1||  +  1)
8.  \mforall{}j:\mBbbN{}||L1||  +  1.  ([x1  /  L1][j]  =  L2[f  j])
9.  increasing(\mlambda{}j.((f  j)  +  1);||L1||  +  1)
10.  j  :  \mBbbN{}||L1||  +  1
\mvdash{}  [x1  /  L1][j]  =  [x2  /  L2][(f  j)  +  1]


By

---

Latex:
Subst  [x2  /  L2][(f  j)  +  1]  =  L2[f  j]  0

---

Home Index