proposition: Lemma inverse_image_fun {X Y : Type} (f : X -> Y) (T : Ensemble Y) : inverse_image f T = fun x => T (f x).
proof: Proof. apply Extensionality_Ensembles. split; red; intros; constructor + destruct H; assumption. Qed.
imports: FunctionProperties Ensembles EnsemblesImplicit EnsemblesSpec IndexedFamilies