---

Step * 1 of Lemma exists_over_implies_push


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)
BY
{ (D (-2) THEN Auto THEN InstConcl [x] THEN Auto) }



1.  T  :  Type@i'
2.  P  :  \mBbbP{}@i'
3.  Q  :  T  {}\mrightarrow{}  \mBbbP{}@i'
4.  \mexists{}x:T.  (P  {}\mRightarrow{}  (Q  x))@i
5.  P@i
\mvdash{}  \mexists{}x:T.  (Q  x)


By

(D  (-2)  THEN  Auto  THEN  InstConcl  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)



Home Index