---

Step * 1 2 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) ⇒ (∀x:T. ((x ∈ remove-first(P;v)) ⇐⇒ (x ∈ v) ∧ (↑¬b(P x))))
⊢ no_repeats(T;[u / v]) ⇒ (∀x:T. ((x ∈ if P u then v else [u / remove-first(P;v)] fi ) ⇐⇒ (x ∈ [u / v]) ∧ (↑¬b(P x))))
BY
{ ((D 0 THENA Auto) THEN (RWO "no_repeats_cons" (-1) THENA Auto) THEN (D -2 THENA Auto)) }

1
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) ∧ (¬(u ∈ v))
7. ∀x:T. ((x ∈ remove-first(P;v)) ⇐⇒ (x ∈ v) ∧ (↑¬b(P x)))
⊢ ∀x:T. ((x ∈ if P u then v else [u / remove-first(P;v)] fi ) ⇐⇒ (x ∈ [u / v]) ∧ (↑¬b(P x)))

---

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)  {}\mRightarrow{}  (\mforall{}x:T.  ((x  \mmember{}  remove-first(P;v))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  v)  \mwedge{}  (\muparrow{}\mneg{}\msubb{}(P  x))))
\mvdash{}  no\_repeats(T;[u  /  v])
{}\mRightarrow{}  (\mforall{}x:T.  ((x  \mmember{}  if  P  u  then  v  else  [u  /  remove-first(P;v)]  fi  )  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  [u  /  v])  \mwedge{}  (\muparrow{}\mneg{}\msubb{}(P  x))))


By

---

Latex:
((D  0  THENA  Auto)  THEN  (RWO  "no\_repeats\_cons"  (-1)  THENA  Auto)  THEN  (D  -2  THENA  Auto))

---

Home Index