---

Step * of Lemma l_subset_pos_length

∀[T:Type]. ∀[A,B:T List].  (0 < ||B||) supposing (0 < ||A|| and l_subset(T;A;B))
BY
{ (InstLemma `l_contains_pos_length` [] THEN RepeatFor 4 (ParallelLast)) }

1
.....antecedent..... 
1. ∀[T:Type]. ∀[A,B:T List].  (0 < ||B||) supposing (0 < ||A|| and A ⊆ B)
2. T : Type
3. ∀[A,B:T List].  (0 < ||B||) supposing (0 < ||A|| and A ⊆ B)
4. A : T List
5. ∀[B:T List]. (0 < ||B||) supposing (0 < ||A|| and A ⊆ B)
6. B : T List
7. l_subset(T;A;B)
⊢ A ⊆ B

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[A,B:T  List].    (0  <  ||B||)  supposing  (0  <  ||A||  and  l\_subset(T;A;B))


By

---

Latex:
(InstLemma  `l\_contains\_pos\_length`  []  THEN  RepeatFor  4  (ParallelLast))

---

Home Index