---

Step * of Lemma first-member-cons

∀[T:Type]
  ∀P:T ⟶ 𝔹. ∀x,u:T. ∀L:T List.  (first-member(T;x;[u / L];P) ⇐⇒ if P u then x = u ∈ T else first-member(T;x;L;P) fi )
BY
{ xxxAutoxxx }

1
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 

2
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)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x,u:T.  \mforall{}L:T  List.
        (first-member(T;x;[u  /  L];P)  \mLeftarrow{}{}\mRightarrow{}  if  P  u  then  x  =  u  else  first-member(T;x;L;P)  fi  )


By

---

Latex:
xxxAutoxxx

---

Home Index