proposition: Lemma in_singleton : forall x y, x \in \{y} = (x = y).
proof: Proof. Proof using. unfold mem, singleton. simpl. intros. rewrite in_single_eq. autos*. Qed.
imports: TLC(LibTactics LibList) TLC(LibSet LibLogic LibEqual LibReflect)