---

Step * of Lemma make-msg-interface-equal

∀[f:Name ─→ Type]. ∀[i1,i2:ℤ]. ∀[l1,l2:Id]. ∀[m1,m2:Message(f)].
  (make-msg-interface(i1;l1;m1) = make-msg-interface(i2;l2;m2) ∈ Interface
  ⇐⇒ (i1 = i2 ∈ ℤ) ∧ (l1 = l2 ∈ Id) ∧ (m1 = m2 ∈ Message(f)))
BY
{ (Auto THEN RepUR ``make-msg-interface`` (-1) THEN EqHD (-1) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[i1,i2:\mBbbZ{}].  \mforall{}[l1,l2:Id].  \mforall{}[m1,m2:Message(f)].
    (make-msg-interface(i1;l1;m1)  =  make-msg-interface(i2;l2;m2)
    \mLeftarrow{}{}\mRightarrow{}  (i1  =  i2)  \mwedge{}  (l1  =  l2)  \mwedge{}  (m1  =  m2))


By

---

Latex:
(Auto  THEN  RepUR  ``make-msg-interface``  (-1)  THEN  EqHD  (-1)  THEN  Auto)

---

Home Index