Nuprl Lemma : msg-body_wf2
[m:Message]. [T:Type]. msg-body(m) 
T supposing 
msg-has-type(m;T)
Proof not projected
Definitions occuring in Statement :
msg-body: msg-body(msg),
msg-has-type: msg-has-type(m;T),
Message: Message,
assert: b,
uimplies: b supposing a,
uall: [x:A]. B[x],
member: t T,
universe: Type
Definitions :
pi2: snd(t),
msg-body: msg-body(msg),
member: t T,
uimplies: b supposing a,
uall: [x:A]. B[x],
pi1: fst(t),
msg-type: msg-type(msg),
mData: mData,
pMsg: pMsg(P.M[P]),
msg-has-type: msg-has-type(m;T),
Message: Message,
prop: 
Lemmas :
Message_wf,
msg-has-type_wf,
assert_wf,
type-valueall-type,
assert-eq_term
\mforall{}[m:Message]. \mforall{}[T:Type]. msg-body(m) \mmember{} T supposing \muparrow{}msg-has-type(m;T)
Date html generated:
2012_01_23-PM-12_46_43
Last ObjectModification:
2011_12_05-PM-12_03_14
Home
Index