proposition: Lemma inverse_image_id {X Y : Type} {f : X -> Y} {g : Y -> X} : (forall y, f (g y) = y) -> forall S, inverse_image g (inverse_image f S) = S.
proof: Proof. intros Hfg S. rewrite <- inverse_image_composition. apply Extensionality_Ensembles. split; red; intros. - destruct H. rewrite <- Hfg. assumption. - constructor. rewrite Hfg. assumption. Qed.
imports: FunctionProperties Ensembles EnsemblesImplicit EnsemblesSpec IndexedFamilies