Nuprl Lemma : msg-has-type-encodes
∀[f,m,T:Top]. (msg-has-type(m;f;T) ~ msg-header(m) encodes T)
Proof
Definitions occuring in Statement :
encodes-msg-type: hdr encodes T,
msg-has-type: msg-has-type(m;f;T),
msg-header: msg-header(m),
uall: ∀[x:A]. B[x],
top: Top,
sqequal: s ~ t
Lemmas :
top_wf
Latex:
\mforall{}[f,m,T:Top]. (msg-has-type(m;f;T) \msim{} msg-header(m) encodes T)
Date html generated:
2015_07_21-PM-04_49_09
Last ObjectModification:
2015_01_28-AM-08_45_12
Home
Index