Nuprl Lemma : vr_parmAC

Nuprl Lemma : vr_parmAC_wf

[A,B:Type].

[G:A

B

]. (vr_parmAC(G;A;B)

')

Proof not projected

Definitions occuring in Statement : vr_parmAC: vr_parmAC(G;A;B), uall:

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

, member: t

T, function: x:A

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

x:A. B[x], uall:

[x:A]. B[x], member: t

T, axiom: Ax, equal: s = t, function: x:A

B[x], vr_parmAC: vr_parmAC(G;A;B), prop:

, implies: P

Q, exists:

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

B[x], all:

x:A. B[x], apply: f a

\mforall{}[A,B:Type]. \mforall{}[G:A {}\mrightarrow{} B {}\mrightarrow{} \mBbbP{}]. (vr\_parmAC(G;A;B) \mmember{} \mBbbU{}') Date html generated: 2012_02_20-PM-03_33_03 Last ObjectModification: 2012_02_02-PM-01_55_15 Home Index