{ 
[hdr:Atom List]. [typ:{T:Type| valueall-type(T)} ]. [val:typ].
(make-Msg(hdr;typ;val) 
Message) }
{ Proof }
Definitions occuring in Statement :
make-Msg: make-Msg(hdr;typ;val),
Message: Message,
uall: [x:A]. B[x],
member: t T,
set: {x:A| B[x]} ,
list: type List,
atom: Atom,
universe: Type,
valueall-type: valueall-type(T)
Lemmas :
valueall-type_wf,
name_wf,
member_wf
\mforall{}[hdr:Atom List]. \mforall{}[typ:\{T:Type| valueall-type(T)\} ]. \mforall{}[val:typ]. (make-Msg(hdr;typ;val) \mmember{} Message)
Date html generated:
2011_08_17-PM-04_06_58
Last ObjectModification:
2011_06_27-PM-05_19_35
Home
Index