---

Step * of Lemma exists_over_implies_push

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

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


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


By

Auto



Home Index