Nuprl Lemma : aa_capply_wf
[a1,a:Type]. [p:a 
]. [l:a 
a1]. (aa_capply(p;l) 
a1 )
Proof
Definitions occuring in Statement :
aa_capply: aa_capply(p;l),
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
int: ,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
aa_capply: aa_capply(p;l),
top: Top,
all: x:A. B[x],
subtype: S 
T,
so_lambda: 
x.t[x],
so_apply: x[s],
guard: {T}
Lemmas :
pi1_wf_top,
pi2_wf,
subtype_rel_self
\mforall{}[a1,a:Type]. \mforall{}[p:a \mtimes{} \mBbbZ{}]. \mforall{}[l:a {}\mrightarrow{} a1]. (aa\_capply(p;l) \mmember{} a1 \mtimes{} \mBbbZ{})
Date html generated:
2013_03_20-AM-09_56_51
Last ObjectModification:
2012_11_27-AM-10_33_45
Home
Index