---

Step * of Lemma length_disjoint_sublists

∀[T:Type]. ∀[L1,L2,L:T List].  (||L1|| + ||L2||) ≤ ||L|| supposing disjoint_sublists(T;L1;L2;L)
BY
{ Auto }

1
1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. disjoint_sublists(T;L1;L2;L)
⊢ (||L1|| + ||L2||) ≤ ||L||

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L1,L2,L:T  List].    (||L1||  +  ||L2||)  \mleq{}  ||L||  supposing  disjoint\_sublists(T;L1;L2;L)


By

---

Latex:
Auto

---

Home Index