---

Step * 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)
⊢ no_repeats(T;L2)
BY
{ (BLemma `no_repeats_iff` THEN Auto THEN AssertBY ⌜x before y ∈ L1⌝ (BackThruSomeHyp THEN Auto)⋅) }

1
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)

---

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)
\mvdash{}  no\_repeats(T;L2)


By

---

Latex:
(BLemma  `no\_repeats\_iff`  THEN  Auto  THEN  AssertBY  \mkleeneopen{}x  before  y  \mmember{}  L1\mkleeneclose{}  (BackThruSomeHyp  THEN  Auto)\mcdot{})

---

Home Index