---

Step * of Lemma atom2-deq-aux

∀[a,b:Atom2].  uiff(a = b ∈ Atom2;↑a =a2 b)
BY
{ Auto }

1
1. a : Atom2
2. b : Atom2
3. ↑a =a2 b
⊢ a = b ∈ Atom2

---

Latex:

---

Latex:
\mforall{}[a,b:Atom2].    uiff(a  =  b;\muparrow{}a  =a2  b)


By

---

Latex:
Auto

---

Home Index