---

Step * of Lemma union-contains

∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List.  as ⊆ as ⋃ bs
BY
{ (Intros THEN (RepUR ``l_contains`` 0 THEN RWO "l_all_iff" 0) THEN Auto THEN RWO "member-union" 0 THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  (RepUR  ``l\_contains``  0  THEN  RWO  "l\_all\_iff"  0)
  THEN  Auto
  THEN  RWO  "member-union"  0
  THEN  Auto)

---

Home Index