proposition: Lemma in_inverse_image {X Y : Type} (f : X -> Y) (T : Ensemble Y) (x : X) : In T (f x) <-> In (inverse_image f T) x.
proof: Proof. rewrite inverse_image_fun. split; auto. Qed.
imports: FunctionProperties Ensembles EnsemblesImplicit EnsemblesSpec IndexedFamilies