Theorem: flatten_atom (Examples.lean)

State before:
atoms : Type u_1
inst✝ : DecidableEq atoms
x : atoms
⊢ flatten (atom x) = {x}
Tactic:
rw [flatten, dif_pos] <;> simp
State after:
no goals