Nuprl Lemma : pax-header2type_wf
[Result:Type]. [hdr:Name]. (pax-header2type(Result;hdr) 
?)
Proof not projected
Definitions occuring in Statement :
pax-header2type: pax-header2type(Result;hdr),
name: Name,
uall: [x:A]. B[x],
prop: ,
unit: Unit,
member: t T,
union: left + right,
universe: Type
Definitions :
product: x:A 
B[x],
list: type List,
name-deq: NameDeq,
pax-message-types: pax-message-types(Result),
apply-alist: apply-alist(eq;L;x),
function: x:A 
B[x],
all: x:A. B[x],
union: left + right,
prop: ,
unit: Unit,
pax-header2type: pax-header2type(Result;hdr),
axiom: Ax,
uall: [x:A]. B[x],
isect: 
x:A. B[x],
name: Name,
universe: Type,
member: t T,
equal: s = t
Lemmas :
apply-alist_wf,
name_wf,
name-deq_wf,
pax-message-types_wf
\mforall{}[Result:Type]. \mforall{}[hdr:Name]. (pax-header2type(Result;hdr) \mmember{} \mBbbP{}?)
Date html generated:
2011_10_20-PM-11_49_53
Last ObjectModification:
2011_05_12-PM-05_43_26
Home
Index