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