---

Step * of Lemma deq-member-union

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:T List]. ∀[x:T].  (x ∈b as ⋃ bs ~ x ∈b as ∨bx ∈b bs)
BY
{ (Auto THEN (BLemma `iff_imp_equal_bool` THENA Auto) THEN (RW assert_pushdownC 0 THENA Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. as : T List
4. bs : T List
5. x : T
⊢ (x ∈ as ⋃ bs) ⇐⇒ (x ∈ as) ∨ (x ∈ bs)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[as,bs:T  List].  \mforall{}[x:T].    (x  \mmember{}\msubb{}  as  \mcup{}  bs  \msim{}  x  \mmember{}\msubb{}  as  \mvee{}\msubb{}x  \mmember{}\msubb{}  bs)


By

---

Latex:
(Auto  THEN  (BLemma  `iff\_imp\_equal\_bool`  THENA  Auto)  THEN  (RW  assert\_pushdownC  0  THENA  Auto))

---

Home Index