---

Step * of Lemma decidable__atom_equal_1

∀a,b:Atom1.  Dec(a = b ∈ Atom1)
BY
{ Auto
THEN Try (Unfold `member` 0
          THEN Refine_atomnEquality)
THEN Unfold `decidable` 0⋅ }

1
1. a : Atom1@i
2. b : Atom1@i
⊢ (a = b ∈ Atom1) ∨ (¬(a = b ∈ Atom1))

---

Latex:

---

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


By

---

Latex:
Auto
THEN  Try  (Unfold  `member`  0
                    THEN  Refine\_atomnEquality)
THEN  Unfold  `decidable`  0\mcdot{}

---

Home Index