---

Step * 2 of Lemma first-member-cons


1. [T] : Type
2. P : T ⟶ 𝔹
3. x : T
4. u : T
5. L : T List
6. if P u then x = u ∈ T else first-member(T;x;L;P) fi 
⊢ first-member(T;x;[u / L];P)
BY
{ xxx(SplitOnHypITE -1  THENA Auto)xxx }

1
.....truecase..... 
1. [T] : Type
2. P : T ⟶ 𝔹
3. x : T
4. u : T
5. L : T List
6. x = u ∈ T
7. ↑(P u)
⊢ first-member(T;x;[u / L];P)

2
.....falsecase..... 
1. [T] : Type
2. P : T ⟶ 𝔹
3. x : T
4. u : T
5. L : T List
6. first-member(T;x;L;P)
7. ¬↑(P u)
⊢ first-member(T;x;[u / L];P)

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(SplitOnHypITE  -1    THENA  Auto)xxx

---

Home Index