proposition: Lemma image_singleton : forall A B (f : A -> B) (x : A), image f \{x} = \{f x}.
proof: Proof. Proof using. intros. apply in_extens. intros z. rewrite in_single_eq. iff N. lets (y&Hy&Ey): in_image_inv (rm N). rewrite in_single_eq in Hy. subst~. applys* in_image_prove. rewrite~ @in_single_eq. typeclass. Qed.
imports: TLC(LibTactics LibLogic LibContainer LibSet)