Nuprl Lemma : msg-type_wf
[m:Message]. (msg-type(m) 
Type)
Proof not projected
Definitions occuring in Statement :
msg-type: msg-type(msg),
Message: Message,
uall: [x:A]. B[x],
member: t T,
universe: Type
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{} Type)
Date html generated:
2012_01_23-PM-12_46_19
Last ObjectModification:
2011_12_05-AM-11_56_37
Home
Index