Nuprl Lemma : TR5a

[T:Type].

[P:T

].

[C:

]. ((

x:T. True)

((

x:T. (P x))

C)

(

x:T. ((P x)

C)))

Proof

Definitions occuring in Statement : uall:

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

, exists:

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

Q, or: P

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

B[x], universe: Type
Definitions : implies: P

Q, member: t

T, so_lambda:

x.t[x], exists:

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

Q, guard: {T}, uall:

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

Lemmas : or_wf, exists_wf, true_wf
\mforall{}[T:Type]. \mforall{}[P:T {}\mrightarrow{} \mBbbP{}]. \mforall{}[C:\mBbbP{}]. ((\mexists{}x:T. True) {}\mRightarrow{} ((\mexists{}x:T. (P x)) \mvee{} C) {}\mRightarrow{} (\mexists{}x:T. ((P x) \mvee{} C))) Date html generated: 2014_07_17-AM-09_55_42 Last ObjectModification: 2014_06_18-PM-02_18_49 Home Index