proposition: Lemma image_union : forall A B (f : A -> B) (E F : set A), image f (E \u F) = image f E \u image f F.
proof: Proof. Proof using. Hint Resolve in_image_prove. introv. apply in_extens. intros x. iff N. lets (y&Hy&Ey): in_image_inv (rm N). rewrite in_union_eq in Hy. rewrite in_union_eq. destruct* Hy. rewrite in_union_eq in N. destruct N as [N|N]. lets (y&Hy&Ey): in_image_inv (rm N). applys* in_image_prove. rewrite in_union_eq. eauto. lets (y&Hy&Ey): in_image_inv (rm N). applys* in_image_prove. rewrite in_union_eq. eauto. Qed.
imports: TLC(LibTactics LibLogic LibContainer LibSet)