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