---

Step * 1 1 of Lemma not_over_forall4


1. T : Type@i'
2. P : T  @i'
3. R:. (R  (R))@i'
4. t:T. (P t)@i
5. (t:T. ((P t)))
 t:T. (P t)
BY
{ (D (-2)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN InstHyp [P t] 3
   THEN Auto
   THEN D (-1)
   THEN Auto
   THEN D (-3)
   THEN InstConcl [t] 
   THEN Auto) }



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


By

(D  (-2)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  InstHyp  [\mkleeneopen{}P  t\mkleeneclose{}]  3\mcdot{}
  THEN  Auto
  THEN  D  (-1)
  THEN  Auto
  THEN  D  (-3)
  THEN  InstConcl  [\mkleeneopen{}t\mkleeneclose{}]  \mcdot{}
  THEN  Auto)\mcdot{}



Home Index