---

Step * of Lemma sq-decider-atom-deq

sq-decider(AtomDeq)
BY
{ (RepUR ``atom-deq sq-decider`` 0 THEN Auto THEN ExRepD) }

1
1. x : Base
2. y : Base
3. z : Base@i
4. x =a y ~ inl z@i
⊢ x = y ∈ Base

---

Latex:

---

Latex:
sq-decider(AtomDeq)


By

---

Latex:
(RepUR  ``atom-deq  sq-decider``  0  THEN  Auto  THEN  ExRepD)

---

Home Index