---

Step * of Lemma test-exists-example2

∀[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. ((R x) ∨ (∃x:D. (Q x)))))
BY
{ (EvidenceTac ⌜λRImpQ,PImpQorR,xP,z. (inr let x = fst(xP) in
                                            let P = snd(xP) in
                                            let QorR = PImpQorR x P in
                                            let isQ = isl(QorR) in
                                            let Q = outl(QorR) in
                                            let R = outr(QorR) in
                                            if isQ then <x, Q> else <x, RImpQ x R> fi  )⌝⋅
   THENA 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{}  (\mforall{}x:D.  ((R  x)  \mvee{}  (\mexists{}x:D.  (Q  x)))))


By

---

Latex:
(EvidenceTac  \mkleeneopen{}\mlambda{}RImpQ,PImpQorR,xP,z.  (inr  let  x  =  fst(xP)  in
                                                                                    let  P  =  snd(xP)  in
                                                                                    let  QorR  =  PImpQorR  x  P  in
                                                                                    let  isQ  =  isl(QorR)  in
                                                                                    let  Q  =  outl(QorR)  in
                                                                                    let  R  =  outr(QorR)  in
                                                                                    if  isQ  then  <x,  Q>  else  <x,  RImpQ  x  R>  fi    )\mkleeneclose{}\mcdot{}
  THENA  Auto
  )

---

Home Index