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