---

Step * of Lemma member-fset-filter

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[P:T ⟶ 𝔹]. ∀[s:fset(T)]. ∀[x:T].  uiff(x ∈ {x ∈ s | P[x]};{x ∈ s ∧ (↑P[x])})
BY
{ (Auto
   THEN All (Unfold `guard`)
   THEN SupposeNot
   THEN Assert ⌜0 = 1 ∈ ℤ⌝⋅
   THEN Auto
   THEN Dquotient2 4
   THEN Auto
   THEN D -1
   THEN All (\h. ((Unfolds ``fset-filter fset-member`` h THEN (RW assert_pushdownC h THENA Auto))
                  THEN Try ((RWO "member_filter" h THENM Reduce h))
                  THEN Auto) )⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[s:fset(T)].  \mforall{}[x:T].
    uiff(x  \mmember{}  \{x  \mmember{}  s  |  P[x]\};\{x  \mmember{}  s  \mwedge{}  (\muparrow{}P[x])\})


By

---

Latex:
(Auto
  THEN  All  (Unfold  `guard`)
  THEN  SupposeNot
  THEN  Assert  \mkleeneopen{}0  =  1\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Dquotient2  4
  THEN  Auto
  THEN  D  -1
  THEN  All  (\mbackslash{}h.  ((Unfolds  ``fset-filter  fset-member``  h  THEN  (RW  assert\_pushdownC  h  THENA  Auto))
                                THEN  Try  ((RWO  "member\_filter"  h  THENM  Reduce  h))
                                THEN  Auto)  )\mcdot{})

---

Home Index