---

Step * of Lemma xmiddle-elim2

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

---

Latex:

---

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


By

---

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

---

Home Index