proposition: Lemma inverse_image_full_set {X Y : Type} (f : X -> Y) : inverse_image f Full_set = Full_set.
proof: Proof. apply Extensionality_Ensembles. split; red; intros; repeat constructor. Qed.
imports: FunctionProperties Ensembles EnsemblesImplicit EnsemblesSpec IndexedFamilies