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