---

Step * 1 of Lemma l_member-iff-length-filter


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)||
BY
{ (Subst ⌜||filter(eq x;L)|| ~ ||filter(λy.(eq x y);L)||⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  eq  :  EqDecider(A)@i
3.  L  :  A  List@i
4.  x  :  A@i
5.  0  <  ||filter(\mlambda{}y.(eqof(eq)  x  y);L)||  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L)
\mvdash{}  1  \mleq{}  ||filter(eq  x;L)||  \mLeftarrow{}{}\mRightarrow{}  0  <  ||filter(\mlambda{}y.(eq  x  y);L)||


By

---

Latex:
(Subst  \mkleeneopen{}||filter(eq  x;L)||  \msim{}  ||filter(\mlambda{}y.(eq  x  y);L)||\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index