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