---

Step * 2 of Lemma not_over_forall3


1. T : Type@i'
2. P : T  @i'
3. R:. (R  (R))@i'
4. t:T. ((P t))@i
 t:T. (P t)
BY
{ (D (-1) THEN D 0 THEN Auto) }



1.  T  :  Type@i'
2.  P  :  T  {}\mrightarrow{}  \mBbbP{}@i'
3.  \mforall{}R:\mBbbP{}.  (\mdownarrow{}R  \mvee{}  (\mneg{}R))@i'
4.  \mexists{}t:T.  (\mneg{}(P  t))@i
\mvdash{}  \mneg{}\mdownarrow{}\mforall{}t:T.  (P  t)


By

(D  (-1)  THEN  D  0  THEN  Auto)



Home Index