---

Step * 2 1 of Lemma remove-first-no_repeats-member


1. ∀[T:Type]
     ∀P:T ⟶ 𝔹
       ((∀a,b:T.  ((↑(P a)) ⇒ (↑(P b)) ⇒ (a = b ∈ T)))
       ⇒ (∀L:T List. (no_repeats(T;L) ⇒ (∀x:T. ((x ∈ remove-first(P;L)) ⇐⇒ (x ∈ L) ∧ (↑¬b(P x)))))))
2. [T] : Type
3. L : T List
4. P : {x:T| (x ∈ L)}  ⟶ 𝔹
5. x : T
6. no_repeats(T;L)
7. ∀a,b:{x:T| (x ∈ L)} .  (((↑(P a)) ∧ (↑(P b))) ⇒ (a = b ∈ T))
8. ∀x:{x:T| (x ∈ L)} . ((x ∈ remove-first(P;L)) ⇐⇒ (x ∈ L) ∧ (↑¬b(P x)))
⊢ (x ∈ remove-first(P;L)) ⇐⇒ (x ∈ L) ∧ (↑¬b(P x))
BY
{ (Auto THEN Try ((FLemma `remove-first-member-implies` [9] THEN Auto)))⋅ }

1
1. ∀[T:Type]
     ∀P:T ⟶ 𝔹
       ((∀a,b:T.  ((↑(P a)) ⇒ (↑(P b)) ⇒ (a = b ∈ T)))
       ⇒ (∀L:T List. (no_repeats(T;L) ⇒ (∀x:T. ((x ∈ remove-first(P;L)) ⇐⇒ (x ∈ L) ∧ (↑¬b(P x)))))))
2. T : Type
3. L : T List
4. P : {x:T| (x ∈ L)}  ⟶ 𝔹
5. x : T
6. no_repeats(T;L)
7. ∀a,b:{x:T| (x ∈ L)} .  (((↑(P a)) ∧ (↑(P b))) ⇒ (a = b ∈ T))
8. ∀x:{x:T| (x ∈ L)} . ((x ∈ remove-first(P;L)) ⇐⇒ (x ∈ L) ∧ (↑¬b(P x)))
9. (x ∈ remove-first(P;L))
10. (x ∈ L)
⊢ ¬↑(P x)

2
1. ∀[T:Type]
     ∀P:T ⟶ 𝔹
       ((∀a,b:T.  ((↑(P a)) ⇒ (↑(P b)) ⇒ (a = b ∈ T)))
       ⇒ (∀L:T List. (no_repeats(T;L) ⇒ (∀x:T. ((x ∈ remove-first(P;L)) ⇐⇒ (x ∈ L) ∧ (↑¬b(P x)))))))
2. [T] : Type
3. L : T List
4. P : {x:T| (x ∈ L)}  ⟶ 𝔹
5. x : T
6. no_repeats(T;L)
7. ∀a,b:{x:T| (x ∈ L)} .  (((↑(P a)) ∧ (↑(P b))) ⇒ (a = b ∈ T))
8. ∀x:{x:T| (x ∈ L)} . ((x ∈ remove-first(P;L)) ⇐⇒ (x ∈ L) ∧ (↑¬b(P x)))
9. (x ∈ L)
10. ↑¬b(P x)
⊢ (x ∈ remove-first(P;L))

---

Latex:

---

Latex:

1.  \mforall{}[T:Type]
          \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}
              ((\mforall{}a,b:T.    ((\muparrow{}(P  a))  {}\mRightarrow{}  (\muparrow{}(P  b))  {}\mRightarrow{}  (a  =  b)))
              {}\mRightarrow{}  (\mforall{}L:T  List
                          (no\_repeats(T;L)  {}\mRightarrow{}  (\mforall{}x:T.  ((x  \mmember{}  remove-first(P;L))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L)  \mwedge{}  (\muparrow{}\mneg{}\msubb{}(P  x)))))))
2.  [T]  :  Type
3.  L  :  T  List
4.  P  :  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}
5.  x  :  T
6.  no\_repeats(T;L)
7.  \mforall{}a,b:\{x:T|  (x  \mmember{}  L)\}  .    (((\muparrow{}(P  a))  \mwedge{}  (\muparrow{}(P  b)))  {}\mRightarrow{}  (a  =  b))
8.  \mforall{}x:\{x:T|  (x  \mmember{}  L)\}  .  ((x  \mmember{}  remove-first(P;L))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L)  \mwedge{}  (\muparrow{}\mneg{}\msubb{}(P  x)))
\mvdash{}  (x  \mmember{}  remove-first(P;L))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L)  \mwedge{}  (\muparrow{}\mneg{}\msubb{}(P  x))


By

---

Latex:
(Auto  THEN  Try  ((FLemma  `remove-first-member-implies`  [9]  THEN  Auto)))\mcdot{}

---

Home Index