---

Step * 1 1 of Lemma scrap1


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)
BY
{ (D (-1) THEN InstConcl [b] THEN Auto THEN OrLeft  THEN Auto) }



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


By

(D  (-1)  THEN  InstConcl  [\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  OrLeft  \mcdot{}  THEN  Auto)



Home Index