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