---

Step * 1 of Lemma es-bound-list


1. es : EO@i'
2. [T] : Type
3. i : Id@i
4. [P] : T ⟶ ℙ
5. [Q] : E ⟶ T ⟶ ℙ
6. ∀x:T. Dec(P[x])@i
7. u : T@i
8. v : T List@i
9. (∀x∈v.P[x] ⇒ (∃e:E. Q[e;x]))
   ⇒ ∃e'@i.True supposing ¬(∃x∈v. P[x])
   ⇒ ∃e'@i.(∀x∈v.P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x]))) 
   supposing (∀x∈v.∀e:E. (Q[e;x] ⇒ (loc(e) = i ∈ Id)))@i
10. (∀x∈[u / v].∀e:E. (Q[e;x] ⇒ (loc(e) = i ∈ Id)))
11. (∀x∈[u / v].P[x] ⇒ (∃e:E. Q[e;x]))@i
12. ∃e'@i.True supposing ¬(∃x∈[u / v]. P[x])@i
⊢ ∃e'@i.(∀x∈[u / v].P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x])))
BY
{ ((D (-4) THENA (RWO "l_all_cons" (-3) THEN Auto)) THEN (D (-1) THENA (RWO "l_all_cons" (-2) THEN Auto))) }

1
1. es : EO@i'
2. [T] : Type
3. i : Id@i
4. [P] : T ⟶ ℙ
5. [Q] : E ⟶ T ⟶ ℙ
6. ∀x:T. Dec(P[x])@i
7. u : T@i
8. v : T List@i
9. (∀x∈[u / v].∀e:E. (Q[e;x] ⇒ (loc(e) = i ∈ Id)))
10. (∀x∈[u / v].P[x] ⇒ (∃e:E. Q[e;x]))@i
11. ∃e'@i.True supposing ¬(∃x∈[u / v]. P[x])@i
12. ∃e'@i.True supposing ¬(∃x∈v. P[x]) ⇒ ∃e'@i.(∀x∈v.P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x])))
⊢ ∃e'@i.(∀x∈[u / v].P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x])))

---

Latex:

---

Latex:

1.  es  :  EO@i'
2.  [T]  :  Type
3.  i  :  Id@i
4.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
5.  [Q]  :  E  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}x:T.  Dec(P[x])@i
7.  u  :  T@i
8.  v  :  T  List@i
9.  (\mforall{}x\mmember{}v.P[x]  {}\mRightarrow{}  (\mexists{}e:E.  Q[e;x]))
      {}\mRightarrow{}  \mexists{}e'@i.True  supposing  \mneg{}(\mexists{}x\mmember{}v.  P[x])
      {}\mRightarrow{}  \mexists{}e'@i.(\mforall{}x\mmember{}v.P[x]  {}\mRightarrow{}  (\mexists{}e:E.  (e  \mleq{}loc  e'    \mwedge{}  Q[e;x]))) 
      supposing  (\mforall{}x\mmember{}v.\mforall{}e:E.  (Q[e;x]  {}\mRightarrow{}  (loc(e)  =  i)))@i
10.  (\mforall{}x\mmember{}[u  /  v].\mforall{}e:E.  (Q[e;x]  {}\mRightarrow{}  (loc(e)  =  i)))
11.  (\mforall{}x\mmember{}[u  /  v].P[x]  {}\mRightarrow{}  (\mexists{}e:E.  Q[e;x]))@i
12.  \mexists{}e'@i.True  supposing  \mneg{}(\mexists{}x\mmember{}[u  /  v].  P[x])@i
\mvdash{}  \mexists{}e'@i.(\mforall{}x\mmember{}[u  /  v].P[x]  {}\mRightarrow{}  (\mexists{}e:E.  (e  \mleq{}loc  e'    \mwedge{}  Q[e;x])))


By

---

Latex:
((D  (-4)  THENA  (RWO  "l\_all\_cons"  (-3)  THEN  Auto))
  THEN  (D  (-1)  THENA  (RWO  "l\_all\_cons"  (-2)  THEN  Auto))
  )

---

Home Index