---

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


1. T : Type
2. P : T ⟶ 𝔹@i
3. ∀a,b:T.  ((↑(P a)) ⇒ (↑(P b)) ⇒ (a = b ∈ T))
4. u : T@i
5. v : T List@i
6. no_repeats(T;v)
7. ¬(u ∈ v)
8. x : T@i
9. (x ∈ remove-first(P;v)) ⇒ ((x ∈ v) ∧ (↑¬b(P x)))
10. (x ∈ remove-first(P;v)) ⇐ (x ∈ v) ∧ (↑¬b(P x))
11. ↑(P u)
12. (x ∈ v)
⊢ ¬↑(P x)
BY
{ (ParallelOp 7 THEN FHyp 3 [-1;-3] THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}@i
3.  \mforall{}a,b:T.    ((\muparrow{}(P  a))  {}\mRightarrow{}  (\muparrow{}(P  b))  {}\mRightarrow{}  (a  =  b))
4.  u  :  T@i
5.  v  :  T  List@i
6.  no\_repeats(T;v)
7.  \mneg{}(u  \mmember{}  v)
8.  x  :  T@i
9.  (x  \mmember{}  remove-first(P;v))  {}\mRightarrow{}  ((x  \mmember{}  v)  \mwedge{}  (\muparrow{}\mneg{}\msubb{}(P  x)))
10.  (x  \mmember{}  remove-first(P;v))  \mLeftarrow{}{}  (x  \mmember{}  v)  \mwedge{}  (\muparrow{}\mneg{}\msubb{}(P  x))
11.  \muparrow{}(P  u)
12.  (x  \mmember{}  v)
\mvdash{}  \mneg{}\muparrow{}(P  x)


By

---

Latex:
(ParallelOp  7  THEN  FHyp  3  [-1;-3]  THEN  Auto)

---

Home Index