---

Step * 1 of Lemma scrap1


1. C : @i'
2. T : Type@i'
3. P : T  @i'
4. a:T. True@i
5. (b:T. ((P b)))  C@i
 b:T. (((P b))  C)
BY
{ (D 4 THEN D 6) }

1
1. C : @i'
2. T : Type@i'
3. P : T  @i'
4. a : T@i
5. True@i
6. b:T. ((P b))@i
 b:T. (((P b))  C)

2
1. C : @i'
2. T : Type@i'
3. P : T  @i'
4. a : T@i
5. True@i
6. C@i
 b:T. (((P b))  C)



1.  C  :  \mBbbP{}@i'
2.  T  :  Type@i'
3.  P  :  T  {}\mrightarrow{}  \mBbbP{}@i'
4.  \mexists{}a:T.  True@i
5.  (\mexists{}b:T.  (\mneg{}(P  b)))  \mvee{}  C@i
\mvdash{}  \mexists{}b:T.  ((\mneg{}(P  b))  \mvee{}  C)


By

(D  4  THEN  D  6)



Home Index