proposition: Lemma notin_singleton_swap : forall x y, x \notin \{y} -> y \notin \{x}.
proof: Proof. Proof using. intros. apply notin_singleton_l. apply sym_not_eq. apply~ notin_singleton_r. Qed.
imports: TLC(LibTactics LibList LibLogic LibNat LibEpsilon LibReflect)