---

Step * of Lemma assert_of_eq_atom1

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

1
1. x : Atom1
2. y : Atom1
3. ↑x =a1 y
⊢ x = y ∈ Atom1

2
1. x : Atom1
2. y : Atom1
3. x = y ∈ Atom1
⊢ ↑x =a1 y

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index