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