Nuprl Lemma : TR1b

[T:Type].

[P:T

].

[C:

]. ((

x:T. (C

(P x)))

C

(

x:T. (P x)))

Proof

Definitions occuring in Statement : uall:

[x:A]. B[x], prop:

, all:

x:A. B[x], implies: P

Q, apply: f a, function: x:A

B[x], universe: Type
Definitions : prop:

, member: t

T, uall:

[x:A]. B[x], implies: P

Q, so_lambda:

x.t[x], subtype_rel: A

r B, all:

x:A. B[x], so_apply: x[s]
Lemmas : all_wf
\mforall{}[T:Type]. \mforall{}[P:T {}\mrightarrow{} \mBbbP{}]. \mforall{}[C:\mBbbP{}]. ((\mforall{}x:T. (C {}\mRightarrow{} (P x))) {}\mRightarrow{} C {}\mRightarrow{} (\mforall{}x:T. (P x))) Date html generated: 2014_07_17-AM-09_55_28 Last ObjectModification: 2014_06_12-PM-04_07_50 Home Index