Nuprl Lemma : Message-eta

[m:Message]. (m = make-Msg(msg-header(m);msg-type(m);msg-body(m)))


Proof not projected



Definitions occuring in Statement :  make-Msg: make-Msg(hdr;typ;val),  msg-header: msg-header(m),  msg-type: msg-type(msg),  msg-body: msg-body(msg),  Message: Message,  uall: [x:A]. B[x],  equal: s = t
Definitions :  uall: [x:A]. B[x],  Message: Message,  make-Msg: make-Msg(hdr;typ;val),  msg-header: msg-header(m),  msg-type: msg-type(msg),  msg-body: msg-body(msg),  pMsg: pMsg(P.M[P]),  mData: mData,  pi1: fst(t),  pi2: snd(t),  member: t  T
Lemmas :  Message_wf
\mforall{}[m:Message].  (m  =  make-Msg(msg-header(m);msg-type(m);msg-body(m)))


Date html generated: 2011_10_20-PM-03_28_58
Last ObjectModification: 2011_09_05-PM-12_47_39

Home Index