---

Step * of Lemma strong-message-constraint-no-rep-implies

∀[f:Name ⟶ Type]. ∀[es:EO+(Message(f))]. ∀[X:EClass(Id × Message(f))]. ∀[hdrs:Name List].
  (strong-message-constraint-no-rep{i:l}(es;X;hdrs;f) ⇒ strong-message-constraint{i:l}(es;X;hdrs;f))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `strong-message-constraint` 0
   THEN Unfold `strong-message-constraint-no-rep` (-1)
   THEN (UnivCD THENA Auto)
   THEN (InstHyp [⌜e⌝] (-2)⋅ THENA Auto)
   THEN SquashExRepD
   THEN D 0
   THEN InstConcl [⌜bg⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[es:EO+(Message(f))].  \mforall{}[X:EClass(Id  \mtimes{}  Message(f))].  \mforall{}[hdrs:Name  List].
    (strong-message-constraint-no-rep\{i:l\}(es;X;hdrs;f)
    {}\mRightarrow{}  strong-message-constraint\{i:l\}(es;X;hdrs;f))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `strong-message-constraint`  0
  THEN  Unfold  `strong-message-constraint-no-rep`  (-1)
  THEN  (UnivCD  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  SquashExRepD
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}bg\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index