---

Step * of Lemma not_over_forall_exists

T1,T2:Type. P:T1  T2  .
  ((R:. (R  (R)))  (t1:T1. (t2:T2. (P t1 t2)))  (t1:T1. (t2:T2. (P t1 t2))))
BY
{ Auto }

1
1. T1 : Type@i'
2. T2 : Type@i'
3. P : T1  T2  @i'
4. R:. (R  (R))@i'
5. t1:T1. (t2:T2. (P t1 t2))@i
 t1:T1. (t2:T2. (P t1 t2))


\mforall{}T1,T2:Type.  \mforall{}P:T1  {}\mrightarrow{}  T2  {}\mrightarrow{}  \mBbbP{}.
    ((\mforall{}R:\mBbbP{}.  (\mdownarrow{}R  \mvee{}  (\mneg{}R)))  {}\mRightarrow{}  (\mneg{}\mdownarrow{}\mforall{}t1:T1.  (\mdownarrow{}\mexists{}t2:T2.  (\mdownarrow{}P  t1  t2)))  {}\mRightarrow{}  (\mdownarrow{}\mexists{}t1:T1.  (\mdownarrow{}\mforall{}t2:T2.  (\mneg{}\mdownarrow{}P  t1  t2))))


By

Auto



Home Index