---

Step * 1 of Lemma first-member-cons


1. [T] : Type
2. P : T ⟶ 𝔹
3. x : T
4. u : T
5. L : T List
6. first-member(T;x;[u / L];P)
⊢ if P u then x = u ∈ T else first-member(T;x;L;P) fi 
BY
{ (D (-1)⋅ THEN CaseNat 0 `i') }

1
1. [T] : Type
2. P : T ⟶ 𝔹
3. x : T
4. u : T
5. L : T List
6. i : ℕ||[u / L]||
7. (x = [u / L][i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P [u / L][j])))
8. i = 0 ∈ ℤ
⊢ if P u then x = u ∈ T else first-member(T;x;L;P) fi 

2
1. [T] : Type
2. P : T ⟶ 𝔹
3. x : T
4. u : T
5. L : T List
6. i : ℕ||[u / L]||
7. (x = [u / L][i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P [u / L][j])))
8. ¬(i = 0 ∈ ℤ)
⊢ if P u then x = u ∈ T else first-member(T;x;L;P) fi 

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  x  :  T
4.  u  :  T
5.  L  :  T  List
6.  first-member(T;x;[u  /  L];P)
\mvdash{}  if  P  u  then  x  =  u  else  first-member(T;x;L;P)  fi 


By

---

Latex:
(D  (-1)\mcdot{}  THEN  CaseNat  0  `i')

---

Home Index