---

Step * of Lemma decidable__atom_equal

∀a,b:Atom.  Dec(a = b ∈ Atom)
BY
{ (Unfold `decidable` 0 THENM (RepD THENA Auto)) }

1
1. a : Atom
2. b : Atom
⊢ (a = b ∈ Atom) ∨ (¬(a = b ∈ Atom))

---

Latex:

---

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


By

---

Latex:
(Unfold  `decidable`  0  THENM  (RepD  THENA  Auto))

---

Home Index