---

Step * 1 1 1 of Lemma not_over_forall_exists_form


1. T1 : Type@i'
2. T2 : Type@i'
3. P : T1  T2  @i'
4. R:. (R  (R))@i'
5. t1 : T1@i
6. t2:T2. (P t1 t2)@i
 t2:T2. (P t1 t2)
BY
{ (Assert (t2:T2. (P t1 t2)) BY
         MaAuto) }

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

2
1. T1 : Type@i'
2. T2 : Type@i'
3. P : T1  T2  @i'
4. R:. (R  (R))@i'
5. t1 : T1@i
6. t2:T2. (P t1 t2)@i
7. (t2:T2. (P t1 t2))
 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.  t1  :  T1@i
6.  \mforall{}t2:T2.  (\mneg{}\mdownarrow{}P  t1  t2)@i
\mvdash{}  \mneg{}\mdownarrow{}\mexists{}t2:T2.  (\mdownarrow{}P  t1  t2)


By

(Assert  \mneg{}(\mexists{}t2:T2.  (\mdownarrow{}P  t1  t2))  BY
              MaAuto)



Home Index