---

Step * of Lemma first-member-iff

∀[T:Type]
  ∀L:T List. ∀P:T ⟶ 𝔹. ∀x:T.
    (first-member(T;x;L;P) ⇐⇒ ∃K,J:T List. ((L = (K @ [x / J]) ∈ (T List)) ∧ (↑(P x)) ∧ (∀y∈K.¬↑(P y))))
BY
{ (Auto THEN All(RepUR ``first-member``) THEN ExRepD) }

1
1. [T] : Type
2. L : T List
3. P : T ⟶ 𝔹
4. x : T
5. i : ℕ||L||
6. x = L[i] ∈ T
7. ↑(P x)
8. ∀j:ℕi. (¬↑(P L[j]))
⊢ ∃K,J:T List. ((L = (K @ [x / J]) ∈ (T List)) ∧ (↑(P x)) ∧ (∀y∈K.¬↑(P y)))

2
1. [T] : Type
2. L : T List
3. P : T ⟶ 𝔹
4. x : T
5. K : T List
6. J : T List
7. L = (K @ [x / J]) ∈ (T List)
8. ↑(P x)
9. (∀y∈K.¬↑(P y))
⊢ ∃i:ℕ||L||. ((x = L[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P L[j]))))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L:T  List.  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}x:T.
        (first-member(T;x;L;P)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}K,J:T  List.  ((L  =  (K  @  [x  /  J]))  \mwedge{}  (\muparrow{}(P  x))  \mwedge{}  (\mforall{}y\mmember{}K.\mneg{}\muparrow{}(P  y))))


By

---

Latex:
(Auto  THEN  All(RepUR  ``first-member``)  THEN  ExRepD)

---

Home Index