---

Step * of Lemma xmiddle-elim

∀[P,Q:ℙ].  (((P ∨ (¬P)) ⇒ (¬Q)) ⇒ (¬Q))
BY
{ ((BasicUniformUnivCD Auto THENA Auto)
   THEN UseWitness ⌜λt,q. (t (inr (λx.(t (inl x) q)) ) q)⌝⋅
   THEN All (RepUR ``not implies``)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P,Q:\mBbbP{}].    (((P  \mvee{}  (\mneg{}P))  {}\mRightarrow{}  (\mneg{}Q))  {}\mRightarrow{}  (\mneg{}Q))


By

---

Latex:
((BasicUniformUnivCD  Auto  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}\mlambda{}t,q.  (t  (inr  (\mlambda{}x.(t  (inl  x)  q))  )  q)\mkleeneclose{}\mcdot{}
  THEN  All  (RepUR  ``not  implies``)
  THEN  Auto)

---

Home Index