---

Step * 1 1 of Lemma first-member-cons


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 
BY
{ (HypSubst' (-1) (-2) THEN Thin (-1) THEN Reduce (-1) THEN AutoSplit) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  x  :  T
4.  u  :  T
5.  L  :  T  List
6.  i  :  \mBbbN{}||[u  /  L]||
7.  (x  =  [u  /  L][i])  \mwedge{}  (\muparrow{}(P  x))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  [u  /  L][j])))
8.  i  =  0
\mvdash{}  if  P  u  then  x  =  u  else  first-member(T;x;L;P)  fi 


By

---

Latex:
(HypSubst'  (-1)  (-2)  THEN  Thin  (-1)  THEN  Reduce  (-1)  THEN  AutoSplit)

---

Home Index