---

Step * of Lemma mem_append

∀s:DSet. ∀as,bs:|s| List. ∀c:|s|.  c ∈b (as @ bs) = (c ∈b as) ∨b(c ∈b bs)
BY
{ ((((RepD THENM BLemma `iff_imp_equal_bool`) THENM RW bool_to_propC 0) THENM RWH (LemmaC `mem_iff_count_nzero`) 0)
   THENA Auto
   ) }

1
1. s : DSet
2. as : |s| List
3. bs : |s| List
4. c : |s|
⊢ (c #∈ (as @ bs)) > 0 ⇐⇒ ((c #∈ as) > 0) ∨ ((c #∈ bs) > 0)

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}as,bs:|s|  List.  \mforall{}c:|s|.    c  \mmember{}\msubb{}  (as  @  bs)  =  (c  \mmember{}\msubb{}  as)  \mvee{}\msubb{}(c  \mmember{}\msubb{}  bs)


By

---

Latex:
((((RepD  THENM  BLemma  `iff\_imp\_equal\_bool`)  THENM  RW  bool\_to\_propC  0)
  THENM  RWH  (LemmaC  `mem\_iff\_count\_nzero`)  0
  )
  THENA  Auto
  )

---

Home Index