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