---

Step * 1 of Lemma not_over_forall_exists


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))
BY
{ ((Assert t1:T1. ((t1.t2:T2. (P t1 t2)) t1) BY
          (BLemma `not_over_forall4` THEN Auto THEN Reduce 0))
   THEN Reduce (-1)
   ) }

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
6. t1:T1. (t2:T2. (P t1 t2))
 t1:T1. (t2:T2. (P t1 t2))



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


By

((Assert  \mdownarrow{}\mexists{}t1:T1.  (\mneg{}\mdownarrow{}(\mlambda{}t1.\mexists{}t2:T2.  (\mdownarrow{}P  t1  t2))  t1)  BY
                (BLemma  `not\_over\_forall4`  THEN  Auto  THEN  Reduce  0))
  THEN  Reduce  (-1)
  )



Home Index