---

Step * 1 of Lemma not_over_forall


1. P:. (P  (P))@i'
2. T : Type@i'
3. P : T  @i'
4. (t:T. (P t))@i
 t:T. ((P t))
BY
{ ((InstHyp [t:T. ((P t))] 1 THEN Auto) THEN D (-1) THEN MaAuto) }

1
1. P:. (P  (P))@i'
2. T : Type@i'
3. P : T  @i'
4. (t:T. (P t))@i
5. (t:T. ((P t)))
 t:T. ((P t))



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


By

((InstHyp  [\mkleeneopen{}\mexists{}t:T.  (\mneg{}(P  t))\mkleeneclose{}]  1\mcdot{}  THEN  Auto)  THEN  D  (-1)  THEN  MaAuto)



Home Index