---

Step * of Lemma not_over_forall4

T:Type. P:T  .  ((R:. (R  (R)))  (t:T. (P t))  (t:T. (P t)))
BY
{ Auto }

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


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


By

Auto



Home Index