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