---

Step * of Lemma cons_sublist_cons

No Annotations
∀[T:Type]. ∀x1,x2:T. ∀L1,L2:T List.  ([x1 / L1] ⊆ [x2 / L2] ⇐⇒ ((x1 = x2 ∈ T) ∧ L1 ⊆ L2) ∨ [x1 / L1] ⊆ L2)
BY
{ (((Auto THEN All (Unfold `sublist`)) THEN All Reduce) THEN ExRepD) }

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)
⊢ ((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))))

2
1. [T] : Type
2. x1 : T
3. x2 : T
4. L1 : T List
5. L2 : T List
6. ((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))))
⊢ ∃f:ℕ||L1|| + 1 ⟶ ℕ||L2|| + 1. (increasing(f;||L1|| + 1) ∧ (∀j:ℕ||L1|| + 1. ([x1 / L1][j] = [x2 / L2][f j] ∈ T)))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type]
    \mforall{}x1,x2:T.  \mforall{}L1,L2:T  List.    ([x1  /  L1]  \msubseteq{}  [x2  /  L2]  \mLeftarrow{}{}\mRightarrow{}  ((x1  =  x2)  \mwedge{}  L1  \msubseteq{}  L2)  \mvee{}  [x1  /  L1]  \msubseteq{}  L2)


By

---

Latex:
(((Auto  THEN  All  (Unfold  `sublist`))  THEN  All  Reduce)  THEN  ExRepD)

---

Home Index