---

Step * 2 2 of Lemma l_find_wf


1. T : Type
2. u : T
3. v : T List
4. ∀[P:{x:T| (x ∈ v)}  ⟶ 𝔹]
     (l_find(v;P) ∈ (∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))])
      ∨ (↓∀i:ℕ||v||. (¬↑(P v[i]))))
5. P : {x:T| (x ∈ [u / v])}  ⟶ 𝔹
6. ¬↑(P u)
7. l_find(v;P) ∈ (∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))]) ∨ (↓∀i:ℕ||v||. (¬↑(P v[i])))
8. l_find(v;P)
= l_find(v;P)
∈ ((∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))]) ∨ (↓∀i:ℕ||v||. (¬↑(P v[i]))))
⊢ ((∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))]) ∨ (↓∀i:ℕ||v||. (¬↑(P v[i])))) ⊆r ((∃x:T
    [(∃i:ℕ||v|| + 1. ((x = [u / v][i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P [u / v][j])))))])
    ∨ (↓∀i:ℕ||v|| + 1. (¬↑(P [u / v][i]))))
BY
{ SubtypeReasoning }

1
.....wf..... 
1. T : Type
2. u : T
3. v : T List
4. ∀[P:{x:T| (x ∈ v)}  ⟶ 𝔹]
     (l_find(v;P) ∈ (∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))])
      ∨ (↓∀i:ℕ||v||. (¬↑(P v[i]))))
5. P : {x:T| (x ∈ [u / v])}  ⟶ 𝔹
6. ¬↑(P u)
7. l_find(v;P) ∈ (∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))]) ∨ (↓∀i:ℕ||v||. (¬↑(P v[i])))
8. l_find(v;P)
= l_find(v;P)
∈ ((∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))]) ∨ (↓∀i:ℕ||v||. (¬↑(P v[i]))))
9. x : ∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))] + (↓∀i:ℕ||v||. (¬↑(P v[i])))
⊢ x ∈ ∃x:T [(∃i:ℕ||v|| + 1. ((x = [u / v][i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P [u / v][j])))))] + (↓∀i:ℕ||v|| + 1
                                                                                                    (¬↑(P [u / v][i])))

2
.....wf..... 
1. T : Type
2. u : T
3. v : T List
4. ∀[P:{x:T| (x ∈ v)}  ⟶ 𝔹]
     (l_find(v;P) ∈ (∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))])
      ∨ (↓∀i:ℕ||v||. (¬↑(P v[i]))))
5. P : {x:T| (x ∈ [u / v])}  ⟶ 𝔹
6. ¬↑(P u)
7. l_find(v;P) ∈ (∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))]) ∨ (↓∀i:ℕ||v||. (¬↑(P v[i])))
8. l_find(v;P)
= l_find(v;P)
∈ ((∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))]) ∨ (↓∀i:ℕ||v||. (¬↑(P v[i]))))
⊢ (∃x:T [(∃i:ℕ||v||. ((x = v[i] ∈ T) ∧ (↑(P x)) ∧ (∀j:ℕi. (¬↑(P v[j])))))]) ∨ (↓∀i:ℕ||v||. (¬↑(P v[i]))) ∈ Type

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  \mforall{}[P:\{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  \mBbbB{}]
          (l\_find(v;P)  \mmember{}  (\mexists{}x:T  [(\mexists{}i:\mBbbN{}||v||.  ((x  =  v[i])  \mwedge{}  (\muparrow{}(P  x))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  v[j])))))])
            \mvee{}  (\mdownarrow{}\mforall{}i:\mBbbN{}||v||.  (\mneg{}\muparrow{}(P  v[i]))))
5.  P  :  \{x:T|  (x  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  \mBbbB{}
6.  \mneg{}\muparrow{}(P  u)
7.  l\_find(v;P)  \mmember{}  (\mexists{}x:T  [(\mexists{}i:\mBbbN{}||v||.  ((x  =  v[i])  \mwedge{}  (\muparrow{}(P  x))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  v[j])))))])
      \mvee{}  (\mdownarrow{}\mforall{}i:\mBbbN{}||v||.  (\mneg{}\muparrow{}(P  v[i])))
8.  l\_find(v;P)  =  l\_find(v;P)
\mvdash{}  ((\mexists{}x:T  [(\mexists{}i:\mBbbN{}||v||.  ((x  =  v[i])  \mwedge{}  (\muparrow{}(P  x))  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  v[j])))))])
        \mvee{}  (\mdownarrow{}\mforall{}i:\mBbbN{}||v||.  (\mneg{}\muparrow{}(P  v[i]))))  \msubseteq{}r  ((\mexists{}x:T  [(\mexists{}i:\mBbbN{}||v||  +  1
                                                                                              ((x  =  [u  /  v][i])
                                                                                              \mwedge{}  (\muparrow{}(P  x))
                                                                                              \mwedge{}  (\mforall{}j:\mBbbN{}i.  (\mneg{}\muparrow{}(P  [u  /  v][j])))))])
        \mvee{}  (\mdownarrow{}\mforall{}i:\mBbbN{}||v||  +  1.  (\mneg{}\muparrow{}(P  [u  /  v][i]))))


By

---

Latex:
SubtypeReasoning

---

Home Index