---

Step * 1 2 of Lemma scrap1


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)
BY
{ (InstConcl [a] THEN Auto THEN OrRight THEN Auto) }



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


By

(InstConcl  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  OrRight  THEN  Auto)



Home Index