---

Step * of Lemma scrap1

C:. T:Type. P:T  .  (((a:T. True)  ((b:T. ((P b)))  C))  (b:T. (((P b))  C)))
BY
{ Auto }

1
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)


\mforall{}C:\mBbbP{}.  \mforall{}T:Type.  \mforall{}P:T  {}\mrightarrow{}  \mBbbP{}.    (((\mexists{}a:T.  True)  \mwedge{}  ((\mexists{}b:T.  (\mneg{}(P  b)))  \mvee{}  C))  {}\mRightarrow{}  (\mexists{}b:T.  ((\mneg{}(P  b))  \mvee{}  C)))


By

Auto



Home Index