Nuprl Lemma : make-Msg_wf

[f:Name ─→ Type]. ∀[hdr:Name]. ∀[val:f hdr].  (make-Msg(hdr;val) ∈ Message(f))


Proof




Definitions occuring in Statement :  make-Msg: make-Msg(hdr;val) Message: Message(f) name: Name uall: [x:A]. B[x] member: t ∈ T apply: a function: x:A ─→ B[x] universe: Type
Lemmas :  bfalse_wf make-basicMsg_wf name_wf

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[hdr:Name].  \mforall{}[val:f  hdr].    (make-Msg(hdr;val)  \mmember{}  Message(f))



Date html generated: 2015_07_21-PM-04_53_23
Last ObjectModification: 2015_01_28-AM-08_42_48

Home Index