Nuprl Lemma : msg-type_wf2

[f:Name ─→ ValueAllType]. ∀[m:Message(f)].  (msg-type(m;f) ∈ {T:Type| valueall-type(T)} )


Proof




Definitions occuring in Statement :  msg-type: msg-type(msg;f) Message: Message(f) name: Name vatype: ValueAllType valueall-type: valueall-type(T) uall: [x:A]. B[x] member: t ∈ T set: {x:A| B[x]}  function: x:A ─→ B[x] universe: Type
Lemmas :  msg-header_wf vatype_wf Message_wf subtype_rel_dep_function name_wf

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  ValueAllType].  \mforall{}[m:Message(f)].    (msg-type(m;f)  \mmember{}  \{T:Type|  valueall-type(T)\}  )



Date html generated: 2015_07_21-PM-04_48_22
Last ObjectModification: 2015_01_28-AM-08_46_32

Home Index