---

Step * of Lemma not_over_forall_form

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{}.    ((\mexists{}t:T.  (\mneg{}(P  t)))  {}\mRightarrow{}  (\mneg{}(\mforall{}t:T.  (P  t))))


By

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



Home Index