Nuprl Lemma : hdrmkmsg_lemma
∀val,hdr,auth:Top. (msg-header(mk-msg(auth;hdr;val)) ~ hdr)
Proof
Definitions occuring in Statement :
mk-msg: mk-msg(auth;hdr;val),
msg-header: msg-header(m),
top: Top,
all: ∀x:A. B[x],
sqequal: s ~ t
Lemmas :
top_wf
Latex:
\mforall{}val,hdr,auth:Top. (msg-header(mk-msg(auth;hdr;val)) \msim{} hdr)
Date html generated:
2015_07_21-PM-04_53_18
Last ObjectModification:
2015_01_28-AM-08_42_37
Home
Index