---

Step * of Lemma length_sublist

∀[T:Type]. ∀[L1,L2:T List].  ||L1|| ≤ ||L2|| supposing L1 ⊆ L2
BY
{ (Unfold `sublist` 0 THEN Auto THEN ExRepD) }

1
1. T : Type
2. L1 : T List
3. L2 : T List
4. f : ℕ||L1|| ⟶ ℕ||L2||
5. increasing(f;||L1||)
6. ∀j:ℕ||L1||. (L1[j] = L2[f j] ∈ T)
⊢ ||L1|| ≤ ||L2||

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L1,L2:T  List].    ||L1||  \mleq{}  ||L2||  supposing  L1  \msubseteq{}  L2


By

---

Latex:
(Unfold  `sublist`  0  THEN  Auto  THEN  ExRepD)

---

Home Index