---

Step * of Lemma make-Msg-as-mk-msg

∀[hdr,val:Top].  (make-Msg(hdr;val) ~ mk-msg(ff;hdr;val))
BY
{ (RepUR ``make-Msg mk-msg`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[hdr,val:Top].    (make-Msg(hdr;val)  \msim{}  mk-msg(ff;hdr;val))


By

---

Latex:
(RepUR  ``make-Msg  mk-msg``  0  THEN  Auto)

---

Home Index