---

Step * 1 1 of Lemma exists_over_implies_pull


1. T : Type@i'
2. P : @i'
3. Q : T  @i'
4. T@i
5. P@i
6. P  (x:T. (Q x))@i
 x:T. (P  (Q x))
BY
{ (RepeatFor 2 ((D (-1) THEN Auto)) THEN InstConcl [x] THEN Auto) }



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


By

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



Home Index