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
Definitions unfolded in proof :
mk-msg: mk-msg(auth;hdr;val),
make-Msg: make-Msg(hdr;val),
uall: ∀[x:A]. B[x],
member: t ∈ T
Latex:
\mforall{}[hdr,val:Top]. (make-Msg(hdr;val) \msim{} mk-msg(ff;hdr;val))
Date html generated:
2016_05_17-AM-08_57_55
Last ObjectModification:
2015_12_29-PM-02_52_35
Theory : messages
Home
Index