---

Step * of Lemma decidable__atom_equal_2

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

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

---

Latex:

---

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


By

---

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

---

Home Index