---

Step * of Lemma test-exists-example1

∀[D:ℙ]. ∀[P,Q,R:D ⟶ ℙ].
  ((∀x:D. ((R x) ⇒ (Q x))) ⇒ (∀x:D. ((P x) ⇒ ((Q x) ∨ (R x)))) ⇒ (∃x:D. (P x)) ⇒ (∃x:D. (Q x)))
BY
{ (EvidenceTac ⌜λRQ,PQorR,xP. let x,P = xP in case PQorR x P of inl(Q) => <x, Q> | inr(R) => <x, RQ x R>⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[D:\mBbbP{}].  \mforall{}[P,Q,R:D  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:D.  ((R  x)  {}\mRightarrow{}  (Q  x)))  {}\mRightarrow{}  (\mforall{}x:D.  ((P  x)  {}\mRightarrow{}  ((Q  x)  \mvee{}  (R  x))))  {}\mRightarrow{}  (\mexists{}x:D.  (P  x))  {}\mRightarrow{}  (\mexists{}x:D.  (Q  x)))


By

---

Latex:
(EvidenceTac  \mkleeneopen{}\mlambda{}RQ,PQorR,xP.  let  x,P  =  xP 
                                                        in  case  PQorR  x  P  of  inl(Q)  =>  <x,  Q>  |  inr(R)  =>  <x,  RQ  x  R>\mkleeneclose{}\mcdot{}
  THEN  Auto
  )

---

Home Index