---

Step * of Lemma l_contains-append

∀[T:Type]. ∀A,B,C:T List.  (A @ B ⊆ C ⇐⇒ A ⊆ C ∧ B ⊆ C)
BY
{ (Intros
   THEN Unfold `l_contains` 0
   THEN (RWO "l_all_iff" 0 THENA Auto)
   THEN RWO "member_append" 0
   THEN Auto
   THEN SplitOrHyps
   THEN Auto') }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}A,B,C:T  List.    (A  @  B  \msubseteq{}  C  \mLeftarrow{}{}\mRightarrow{}  A  \msubseteq{}  C  \mwedge{}  B  \msubseteq{}  C)


By

---

Latex:
(Intros
  THEN  Unfold  `l\_contains`  0
  THEN  (RWO  "l\_all\_iff"  0  THENA  Auto)
  THEN  RWO  "member\_append"  0
  THEN  Auto
  THEN  SplitOrHyps
  THEN  Auto')

---

Home Index