---

Step * of Lemma test-evd3

∀[D:ℙ]. ∀[P,Q:D ⟶ ℙ].  ((∀x:D. ((P x) ⇒ (Q x))) ⇒ (∃x:D. (P x)) ⇒ (∃x:D. (Q x)))
BY
{ (EvidenceTac ⌜λf,p. let x,y = p in <x, f x y>⌝⋅ THENA Auto) }

---

Latex:

---

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


By

---

Latex:
(EvidenceTac  \mkleeneopen{}\mlambda{}f,p.  let  x,y  =  p  in  <x,  f  x  y>\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index