Nuprl Lemma : make-Msg-equal

[hdr,hdr2:Atom List].

[typ,typ2:{T:Type| valueall-type(T)} ].

[val:typ].

[val2:typ2].
(make-Msg(hdr;typ;val) = make-Msg(hdr2;typ2;val2)

{(hdr = hdr2)

(typ = typ2)

(val = val2)})

Proof not projected

Definitions occuring in Statement : make-Msg: make-Msg(hdr;typ;val), Message: Message, name: Name, uall:

[x:A]. B[x], guard: {T}, iff: P

Q, and: P

Q, set: {x:A| B[x]} , list: type List, atom: Atom, universe: Type, equal: s = t, valueall-type: valueall-type(T)
Definitions : uall:

[x:A]. B[x], iff: P

Q, guard: {T}, and: P

Q, name: Name, member: t

T, implies: P

Q, rev_implies: P

Q, prop:

, cand: A c

B, so_lambda:

x.t[x], top: Top, all:

x:A. B[x], subtype: S

T, squash:

T, true: True, Message: Message, make-Msg: make-Msg(hdr;typ;val), pMsg: pMsg(P.M[P]), mData: mData, pi2: snd(t), so_apply: x[s], pi1: fst(t)
Lemmas : equal_wf, Message_wf, make-Msg_wf, name_wf, valueall-type_wf, pi2_wf, mData_wf, pi1_wf_top, squash_wf, true_wf, member_wf

\mforall{}[hdr,hdr2:Atom List]. \mforall{}[typ,typ2:\{T:Type| valueall-type(T)\} ]. \mforall{}[val:typ]. \mforall{}[val2:typ2]. (make-Msg(hdr;typ;val) = make-Msg(hdr2;typ2;val2) \mLeftarrow{}{}\mRightarrow{} \{(hdr = hdr2) \mwedge{} (typ = typ2) \mwedge{} (val = val2)\}) Date html generated: 2012_01_23-PM-12_50_31 Last ObjectModification: 2012_01_06-PM-03_31_20 Home Index