Nuprl Lemma : aa_capply_wf2
p:Base 
. l:Base 
Base. (aa_capply(p;l) 
Base )
Proof
Definitions occuring in Statement :
aa_capply: aa_capply(p;l),
nat: ,
all: x:A. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
base: Base
Definitions :
all: x:A. B[x],
nat: ,
member: t T,
aa_capply: aa_capply(p;l),
top: Top,
subtype: S 
T,
so_lambda: 
x.t[x],
uall: [x:A]. B[x],
so_apply: x[s],
guard: {T}
Lemmas :
pi1_wf_top,
nat_wf,
pi2_wf,
base_wf,
subtype_rel_set_simple,
le_wf
\mforall{}p:Base \mtimes{} \mBbbN{}. \mforall{}l:Base {}\mrightarrow{} Base. (aa\_capply(p;l) \mmember{} Base \mtimes{} \mBbbN{})
Date html generated:
2013_03_20-AM-09_56_55
Last ObjectModification:
2012_11_27-AM-10_33_46
Home
Index