---

Step * of Lemma find_property

∀[T:Type]
  ∀P:T ⟶ 𝔹. ∀as:T List. ∀d:T.  (((first a ∈ as s.t. P[a] else d) ∈ as) ∨ ((first a ∈ as s.t. P[a] else d) = d ∈ T))
BY
{ (((InductionOnList THEN Unfold `find` 0 THEN Reduce 0 THEN Try (SimpConcl) THEN SplitOnConclITE) THENA Auto{1,3}-1)
   THEN Reduce 0
   THEN Try (Fold `find` 0)) }

1
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀d:T. (((first a ∈ v s.t. P[a] else d) ∈ v) ∨ ((first a ∈ v s.t. P[a] else d) = d ∈ T))
6. ↑P[u]
⊢ ∀d:T. ((u ∈ [u / v]) ∨ (u = d ∈ T))

2
1. [T] : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ∀d:T. (((first a ∈ v s.t. P[a] else d) ∈ v) ∨ ((first a ∈ v s.t. P[a] else d) = d ∈ T))
6. ¬↑P[u]
⊢ ∀d:T. (((first a ∈ v s.t. P[a] else d) ∈ [u / v]) ∨ ((first a ∈ v s.t. P[a] else d) = d ∈ T))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}as:T  List.  \mforall{}d:T.
        (((first  a  \mmember{}  as  s.t.  P[a]  else  d)  \mmember{}  as)  \mvee{}  ((first  a  \mmember{}  as  s.t.  P[a]  else  d)  =  d))


By

---

Latex:
(((InductionOnList  THEN  Unfold  `find`  0  THEN  Reduce  0  THEN  Try  (SimpConcl)  THEN  SplitOnConclITE)
    THENA  Auto\{1,3\}-1
    )
  THEN  Reduce  0
  THEN  Try  (Fold  `find`  0))

---

Home Index