---

Step * of Lemma l-union-contained

∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs,cs:T List.  (as ⋃ bs ⊆ cs ⇐⇒ as ⊆ cs ∧ bs ⊆ cs)
BY
{ (((UnivCD THENA Auto) THEN Unfold `l_contains` 0)
   THEN (All (RWO "l_all_iff") THENA Auto)
   THEN RWO "member-union" 0
   THEN Auto
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}as,bs,cs:T  List.    (as  \mcup{}  bs  \msubseteq{}  cs  \mLeftarrow{}{}\mRightarrow{}  as  \msubseteq{}  cs  \mwedge{}  bs  \msubseteq{}  cs)


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  Unfold  `l\_contains`  0)
  THEN  (All  (RWO  "l\_all\_iff")  THENA  Auto)
  THEN  RWO  "member-union"  0
  THEN  Auto
  THEN  D  -1
  THEN  Auto)

---

Home Index