Nuprl Lemma : vr_AC1

vr_AC1

{i''}

Proof not projected

Definitions occuring in Statement : vr_AC1: vr_AC1, member: t

T, universe: Type
Definitions : tactic: Error :tactic, member: t

T, isect:

x:A. B[x], uall:

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

B[x], all:

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

, apply: f a, product: x:A

B[x], exists:

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

Q, so_lambda:

x.t[x], equal: s = t, vr_AC1: vr_AC1, lambda:

x.A[x]
Lemmas : uall_wf

vr\_AC1 \mmember{} \mBbbU{}\{i''\} Date html generated: 2012_02_20-PM-03_33_25 Last ObjectModification: 2012_02_02-PM-01_55_20 Home Index