---

Step * of Lemma assert_of_eq_atom2

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

1
1. x : Atom2
2. y : Atom2
3. ↑x =a2 y
⊢ x = y ∈ Atom2

2
1. x : Atom2
2. y : Atom2
3. x = y ∈ Atom2
⊢ ↑x =a2 y

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index