Step * of Lemma l_member-iff-length-filter

`∀[A:Type]. ∀eq:EqDecider(A). ∀L:A List. ∀x:A.  (1 ≤ ||filter(eq x;L)|| `⇐⇒` (x ∈ L))`
BY
`{ (((UnivCD THENA Auto) THEN (InstLemma `assert-deq-member` [⌜A⌝;⌜eq⌝;⌜L⌝;⌜x⌝]⋅ THENA Auto))`
`   THEN (RWO "deq-member-length-filter2" (-1) THENA Auto)`
`   THEN (RW assert_pushdownC (-1) THENA Auto)`
`   THEN (RWO "-1<" 0 THENA Auto)`
`   THEN RepUR ``eqof`` 0) }`

1
`1. [A] : Type`
`2. eq : EqDecider(A)@i`
`3. L : A List@i`
`4. x : A@i`
`5. 0 < ||filter(λy.(eqof(eq) x y);L)|| `⇐⇒` (x ∈ L)`
`⊢ 1 ≤ ||filter(eq x;L)|| `⇐⇒` 0 < ||filter(λy.(eq x y);L)||`

Latex:

Latex:
\mforall{}[A:Type].  \mforall{}eq:EqDecider(A).  \mforall{}L:A  List.  \mforall{}x:A.    (1  \mleq{}  ||filter(eq  x;L)||  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L))

By

Latex:
(((UnivCD  THENA  Auto)  THEN  (InstLemma  `assert-deq-member`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto))
THEN  (RWO  "deq-member-length-filter2"  (-1)  THENA  Auto)
THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
THEN  (RWO  "-1<"  0  THENA  Auto)
THEN  RepUR  ``eqof``  0)

Home Index