---

Step * 1 1 2 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|| + 1
7. increasing(f;||L1|| + 1)
8. ∀j:ℕ||L1|| + 1. ([x1 / L1][j] = [x2 / L2][f j] ∈ T)
9. [x1 / L1][0] = [x2 / L2][f 0] ∈ T
10. f 0 ≠ 0
⊢ ((x1 = x2 ∈ T) ∧ (∃f:ℕ||L1|| ⟶ ℕ||L2||. (increasing(f;||L1||) ∧ (∀j:ℕ||L1||. (L1[j] = L2[f j] ∈ T)))))
∨ (∃f:ℕ||L1|| + 1 ⟶ ℕ||L2||. (increasing(f;||L1|| + 1) ∧ (∀j:ℕ||L1|| + 1. ([x1 / L1][j] = L2[f j] ∈ T))))
BY
{ ((OrRight THENA Auto) THEN InstConcl [λj.((f j) - 1)] THEN Auto) }

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

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

3
1. T : Type
2. x1 : T
3. x2 : T
4. L1 : T List
5. L2 : T List
6. f : ℕ||L1|| + 1 ⟶ ℕ||L2|| + 1
7. increasing(f;||L1|| + 1)
8. ∀j:ℕ||L1|| + 1. ([x1 / L1][j] = [x2 / L2][f j] ∈ T)
9. [x1 / L1][0] = [x2 / L2][f 0] ∈ T
10. f 0 ≠ 0
11. increasing(λj.((f j) - 1);||L1|| + 1)
12. j : ℕ||L1|| + 1
⊢ [x1 / L1][j] = L2[(λj.((f j) - 1)) j] ∈ 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||  +  1
7.  increasing(f;||L1||  +  1)
8.  \mforall{}j:\mBbbN{}||L1||  +  1.  ([x1  /  L1][j]  =  [x2  /  L2][f  j])
9.  [x1  /  L1][0]  =  [x2  /  L2][f  0]
10.  f  0  \mneq{}  0
\mvdash{}  ((x1  =  x2)  \mwedge{}  (\mexists{}f:\mBbbN{}||L1||  {}\mrightarrow{}  \mBbbN{}||L2||.  (increasing(f;||L1||)  \mwedge{}  (\mforall{}j:\mBbbN{}||L1||.  (L1[j]  =  L2[f  j])))))
\mvee{}  (\mexists{}f:\mBbbN{}||L1||  +  1  {}\mrightarrow{}  \mBbbN{}||L2||
        (increasing(f;||L1||  +  1)  \mwedge{}  (\mforall{}j:\mBbbN{}||L1||  +  1.  ([x1  /  L1][j]  =  L2[f  j]))))


By

---

Latex:
((OrRight  THENA  Auto)  THEN  InstConcl  [\mlambda{}j.((f  j)  -  1)]  THEN  Auto)

---

Home Index