Step
*
of Lemma
squash_thru_implies_dec
∀[P,Q:ℙ]. uiff(↓P
⇒ Q;P
⇒ (↓Q)) supposing Dec(P)
BY
{ (Auto THEN D -2 THEN Try ((D 0 THEN Complete (Auto))) THEN ThinTrivial THEN Auto THEN D 0 THEN Auto) }
Latex:
Latex:
\mforall{}[P,Q:\mBbbP{}]. uiff(\mdownarrow{}P {}\mRightarrow{} Q;P {}\mRightarrow{} (\mdownarrow{}Q)) supposing Dec(P)
By
Latex:
(Auto THEN D -2 THEN Try ((D 0 THEN Complete (Auto))) THEN ThinTrivial THEN Auto THEN D 0 THEN Auto)
Home
Index