Nuprl Lemma : cdv-argtype_wf
[d:ClassDerivation]. (cdv-argtype(d) 
Type)
Proof not projected
Definitions occuring in Statement :
cdv-argtype: cdv-argtype(dv),
classderiv: ClassDerivation,
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
false: False,
implies: P 
Q,
not: 
A,
le: A 
B,
let: let,
cdv-argtype: cdv-argtype(dv),
member: t T,
uall: [x:A]. B[x],
and: P 
Q,
lelt: i j < k,
uimplies: b supposing a,
int_seg: {i..j
}
Lemmas :
classderiv_wf,
select_wf,
bag_wf,
cdv-types_wf,
length_wf,
int_seg_wf
\mforall{}[d:ClassDerivation]. (cdv-argtype(d) \mmember{} Type)
Date html generated:
2012_01_23-PM-12_52_07
Last ObjectModification:
2011_12_11-PM-12_19_28
Home
Index