---

Step * 1 of Lemma l_subset_pos_length

.....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
BY
{ (RWO "l_subset-l_contains" (-1) THEN Auto) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  \mforall{}[T:Type].  \mforall{}[A,B:T  List].    (0  <  ||B||)  supposing  (0  <  ||A||  and  A  \msubseteq{}  B)
2.  T  :  Type
3.  \mforall{}[A,B:T  List].    (0  <  ||B||)  supposing  (0  <  ||A||  and  A  \msubseteq{}  B)
4.  A  :  T  List
5.  \mforall{}[B:T  List].  (0  <  ||B||)  supposing  (0  <  ||A||  and  A  \msubseteq{}  B)
6.  B  :  T  List
7.  l\_subset(T;A;B)
\mvdash{}  A  \msubseteq{}  B


By

---

Latex:
(RWO  "l\_subset-l\_contains"  (-1)  THEN  Auto)

---

Home Index