---

Step * of Lemma exists_over_implies_pull

T:Type. P:. Q:T  .  (T  Dec(P)  (P  (x:T. (Q x)))  (x:T. (P  (Q x))))
BY
{ Auto }

1
1. T : Type@i'
2. P : @i'
3. Q : T  @i'
4. T@i
5. Dec(P)@i
6. P  (x:T. (Q x))@i
 x:T. (P  (Q x))


\mforall{}T:Type.  \mforall{}P:\mBbbP{}.  \mforall{}Q:T  {}\mrightarrow{}  \mBbbP{}.    (T  {}\mRightarrow{}  Dec(P)  {}\mRightarrow{}  (P  {}\mRightarrow{}  (\mexists{}x:T.  (Q  x)))  {}\mRightarrow{}  (\mexists{}x:T.  (P  {}\mRightarrow{}  (Q  x))))


By

Auto



Home Index