---

Step * of Lemma decidable__equal_Id

∀a,b:Id.  Dec(a = b ∈ Id)
BY
{ (RWO "assert-eq-id<" 0 THENA Auto) }

1
∀a,b:Id.  Dec(↑a = b)

---

Latex:

---

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


By

---

Latex:
(RWO  "assert-eq-id<"  0  THENA  Auto)

---

Home Index