---

Step * of Lemma decidable__equal_IdLnk

∀a,b:IdLnk.  Dec(a = b ∈ IdLnk)
BY
{ (RWO "assert-eq-lnk<" 0 THEN Auto) }

---

Latex:


\mforall{}a,b:IdLnk.    Dec(a  =  b)


By

(RWO  "assert-eq-lnk<"  0  THEN  Auto)

---

Home Index