Nuprl Lemma : disjoint-union-type_wf
[L:Type List]. (disjoint-union-type(L) 
Type)
Proof not projected
Definitions occuring in Statement :
disjoint-union-type: disjoint-union-type(L),
uall: [x:A]. B[x],
member: t T,
list: type List,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
disjoint-union-type: disjoint-union-type(L),
top: Top,
all: x:A. B[x],
subtype: S 
T
Lemmas :
unit_wf2,
ifthenelse_wf,
null_wf3,
top_wf
\mforall{}[L:Type List]. (disjoint-union-type(L) \mmember{} Type)
Date html generated:
2011_10_20-PM-03_39_30
Last ObjectModification:
2011_09_23-PM-06_46_18
Home
Index