Nuprl Lemma : Message_wf

[f:Name ─→ Type]. (Message(f) ∈ Type)


Proof




Definitions occuring in Statement :  Message: Message(f) name: Name uall: [x:A]. B[x] member: t ∈ T function: x:A ─→ B[x] universe: Type
Lemmas :  bool_wf basicMessage_wf name_wf

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  (Message(f)  \mmember{}  Type)



Date html generated: 2015_07_21-PM-04_48_12
Last ObjectModification: 2015_01_28-AM-08_46_41

Home Index