---

Step * of Lemma l-union_functionality_wrt-l_contains

∀[T:Type]. ∀eq:EqDecider(T). ∀as1,bs1,as2,bs2:T List.  (bs1 ⊆ bs2 ⇒ as1 ⊆ as2 ⇒ as1 ⋃ bs1 ⊆ as2 ⋃ bs2)
BY
{ ((Auto THEN All  (Unfold `l_contains`)⋅)
   THEN (All (RWO "l_all_iff") THENA Auto)
   THEN RWO "member-union" 0
   THEN Auto
   THEN ParallelLast
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}as1,bs1,as2,bs2:T  List.    (bs1  \msubseteq{}  bs2  {}\mRightarrow{}  as1  \msubseteq{}  as2  {}\mRightarrow{}  as1  \mcup{}  bs1  \msubseteq{}  as2  \mcup{}  bs2)


By

---

Latex:
((Auto  THEN  All    (Unfold  `l\_contains`)\mcdot{})
  THEN  (All  (RWO  "l\_all\_iff")  THENA  Auto)
  THEN  RWO  "member-union"  0
  THEN  Auto
  THEN  ParallelLast
  THEN  Auto)

---

Home Index