---

Step * of Lemma dest_mk_prec_lemma

∀x,lbl:Top.  (dest-prec(mk-prec(lbl;x)) ~ <lbl, x>)
BY
{ (Auto THEN Computation) }

---

Latex:

---

Latex:
\mforall{}x,lbl:Top.    (dest-prec(mk-prec(lbl;x))  \msim{}  <lbl,  x>)


By

---

Latex:
(Auto  THEN  Computation)

---

Home Index