---

Step * of Lemma not_over_forall_form_squash

T:Type. P:T  .  ((t:T. (P t))  (t:T. (P t)))
BY
{ (Auto THEN D (-1) THEN D 0 THEN Auto) }


\mforall{}T:Type.  \mforall{}P:T  {}\mrightarrow{}  \mBbbP{}.    ((\mdownarrow{}\mexists{}t:T.  (\mneg{}\mdownarrow{}P  t))  {}\mRightarrow{}  (\mneg{}\mdownarrow{}\mforall{}t:T.  (\mdownarrow{}P  t)))


By

(Auto\mcdot{}  THEN  D  (-1)  THEN  D  0  THEN  Auto)



Home Index