---

Step * 1 1 of Lemma l_contains_pos_length


1. T : Type
2. A : T List
3. B : T List
4. (∀a∈A.(a ∈ B))
5. ¬↑null(A)
⊢ ¬↑null(B)
BY
{ TACTIC:(DVar `A' THEN All Reduce THEN Auto THEN (With ⌜0⌝ (D (-2))⋅ THENA Auto') THEN RepeatFor 2 (D -1) THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  A  :  T  List
3.  B  :  T  List
4.  (\mforall{}a\mmember{}A.(a  \mmember{}  B))
5.  \mneg{}\muparrow{}null(A)
\mvdash{}  \mneg{}\muparrow{}null(B)


By

---

Latex:
TACTIC:(DVar  `A'
                THEN  All  Reduce
                THEN  Auto
                THEN  (With  \mkleeneopen{}0\mkleeneclose{}  (D  (-2))\mcdot{}  THENA  Auto')
                THEN  RepeatFor  2  (D  -1)
                THEN  Auto')

---

Home Index