Nuprl Lemma : make-Msg-equal
∀[f:Name ─→ Type]. ∀[hdr1,hdr2:Name]. ∀[val1:f hdr1]. ∀[val2:f hdr2].
(make-Msg(hdr1;val1) = make-Msg(hdr2;val2) ∈ Message(f) ⇐⇒ {(hdr1 = hdr2 ∈ Name) ∧ (val1 = val2 ∈ (f hdr1))})
Proof
Definitions occuring in Statement :
make-Msg: make-Msg(hdr;val),
Message: Message(f),
name: Name,
uall: ∀[x:A]. B[x],
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ─→ B[x],
universe: Type,
equal: s = t ∈ T
Lemmas :
and_wf,
equal_wf,
name_wf,
pi1_wf_top,
subtype_rel_product,
top_wf,
subtype_top,
Message_wf,
make-Msg_wf,
subtype_rel_self,
subtype_rel_wf,
subtype_base_sq,
list_subtype_base,
atom_subtype_base
Latex:
\mforall{}[f:Name {}\mrightarrow{} Type]. \mforall{}[hdr1,hdr2:Name]. \mforall{}[val1:f hdr1]. \mforall{}[val2:f hdr2].
(make-Msg(hdr1;val1) = make-Msg(hdr2;val2) \mLeftarrow{}{}\mRightarrow{} \{(hdr1 = hdr2) \mwedge{} (val1 = val2)\})
Date html generated:
2015_07_21-PM-04_53_25
Last ObjectModification:
2015_01_28-AM-08_44_42
Home
Index