---

Step * of Lemma eq_atom_eq_false_elim

∀[x,y:Atom].  ¬(x = y ∈ Atom) supposing x =a y = ff
BY
{ Auto }

1
1. x : Atom
2. y : Atom
3. x =a y = ff
⊢ ¬(x = y ∈ Atom)

---

Latex:

---

Latex:
\mforall{}[x,y:Atom].    \mneg{}(x  =  y)  supposing  x  =a  y  =  ff


By

---

Latex:
Auto

---

Home Index