---

Step * of Lemma not_over_forall

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

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

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


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


By

Auto



Home Index