---

Step * 1 2 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
{ (RenameVar `t' (-3) THEN InstConcl [t] THEN Auto) }



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


By

(RenameVar  `t'  (-3)  THEN  InstConcl  [\mkleeneopen{}t\mkleeneclose{}]\mcdot{}  THEN  Auto)



Home Index