---

Step * 1 1 1 of Lemma bag-member-filter-implies2


1. [T] : Type
2. b1 : T List
3. x1 : {x:T| x ↓∈ b1}  ⟶ 𝔹
4. x : T
5. x ↓∈ [x∈b1|x1[x]]
⊢ Ax ∈ x ↓∈ b1
BY
{ (RepUR ``bag-filter bag-member`` (-1)
   THEN (TrySquashExRepD (-1) THENA Auto)
   THEN (EqTypeHD (-2) THENA EAuto 2)
   THEN (Unhide THENA Auto)
   THEN (FLemma `member-permutation` [-2]
         THENA (Try (Complete (Auto))
                THEN InstLemma `filter_wf2` [⌜T⌝;⌜b1⌝;⌜λx.x1[x]⌝]⋅
                THEN Try (Complete (Auto))
                THEN Auto
                THEN DVarSets
                THEN MemTypeCD
                THEN Auto
                THEN BLemma `list-member-bag-member`
                THEN Auto)
         )
   THEN (RWO "-1" (-2) THENA Auto)
   THEN RWO "member_filter_2" (-2)
   THEN Auto
   THEN Try (Complete ((BLemma `bag-member-evidence` THEN Auto THEN BLemma `list-member-bag-member` THEN Auto)))
   THEN DVarSets
   THEN MemTypeCD
   THEN Auto
   THEN BLemma `list-member-bag-member`
   THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  b1  :  T  List
3.  x1  :  \{x:T|  x  \mdownarrow{}\mmember{}  b1\}    {}\mrightarrow{}  \mBbbB{}
4.  x  :  T
5.  x  \mdownarrow{}\mmember{}  [x\mmember{}b1|x1[x]]
\mvdash{}  Ax  \mmember{}  x  \mdownarrow{}\mmember{}  b1


By

---

Latex:
(RepUR  ``bag-filter  bag-member``  (-1)
  THEN  (TrySquashExRepD  (-1)  THENA  Auto)
  THEN  (EqTypeHD  (-2)  THENA  EAuto  2)
  THEN  (Unhide  THENA  Auto)
  THEN  (FLemma  `member-permutation`  [-2]
              THENA  (Try  (Complete  (Auto))
                            THEN  InstLemma  `filter\_wf2`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}\mlambda{}x.x1[x]\mkleeneclose{}]\mcdot{}
                            THEN  Try  (Complete  (Auto))
                            THEN  Auto
                            THEN  DVarSets
                            THEN  MemTypeCD
                            THEN  Auto
                            THEN  BLemma  `list-member-bag-member`
                            THEN  Auto)
              )
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  THEN  RWO  "member\_filter\_2"  (-2)
  THEN  Auto
  THEN  Try  (Complete  ((BLemma  `bag-member-evidence`
                                            THEN  Auto
                                            THEN  BLemma  `list-member-bag-member`
                                            THEN  Auto)))
  THEN  DVarSets
  THEN  MemTypeCD
  THEN  Auto
  THEN  BLemma  `list-member-bag-member`
  THEN  Auto)

---

Home Index