---

Step * 1 of Lemma exists_over_implies_pull


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))
BY
{ (Unfold `decidable` (-2) THEN D (-2)) }

1
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))

2
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))



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


By

(Unfold  `decidable`  (-2)  THEN  D  (-2))



Home Index