---

Step * 1 1 of Lemma implies-filter-equal


1. T : Type
2. P : T ⟶ 𝔹
3. L1 : T List
4. L2 : T List
5. no_repeats(T;L1)
6. ∀x:T. ((x ∈ L2) ⇐⇒ (x ∈ L1) ∧ (↑(P x)))
7. ∀x,y:T.  (x before y ∈ L2 ⇒ x before y ∈ L1)
8. x : T
9. y : T
10. x before y ∈ L2
11. x before y ∈ L1
⊢ ¬(x = y ∈ T)
BY
{ ∀h:hyp. (RWO "no_repeats_iff" h THEN Auto THEN BHyp h THEN Auto)  }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  L1  :  T  List
4.  L2  :  T  List
5.  no\_repeats(T;L1)
6.  \mforall{}x:T.  ((x  \mmember{}  L2)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L1)  \mwedge{}  (\muparrow{}(P  x)))
7.  \mforall{}x,y:T.    (x  before  y  \mmember{}  L2  {}\mRightarrow{}  x  before  y  \mmember{}  L1)
8.  x  :  T
9.  y  :  T
10.  x  before  y  \mmember{}  L2
11.  x  before  y  \mmember{}  L1
\mvdash{}  \mneg{}(x  =  y)


By

---

Latex:
\mforall{}h:hyp.  (RWO  "no\_repeats\_iff"  h  THEN  Auto  THEN  BHyp  h  THEN  Auto) 

---

Home Index