Nuprl Lemma : msg-type_wf2
[m:Message]. (msg-type(m) 
{T:Type| valueall-type(T)} )
Proof not projected
Definitions occuring in Statement :
msg-type: msg-type(msg),
Message: Message,
uall: [x:A]. B[x],
member: t T,
set: {x:A| B[x]} ,
universe: Type,
valueall-type: valueall-type(T)
Definitions :
pi2: snd(t),
pi1: fst(t),
msg-type: msg-type(msg),
member: t T,
uall: [x:A]. B[x],
mData: mData,
pMsg: pMsg(P.M[P]),
Message: Message
Lemmas :
Message_wf
\mforall{}[m:Message]. (msg-type(m) \mmember{} \{T:Type| valueall-type(T)\} )
Date html generated:
2012_01_23-PM-12_46_30
Last ObjectModification:
2011_12_05-PM-07_27_00
Home
Index