proposition: Lemma sig_fn_extend_range {X Y : Type} {P : X -> Prop} (f : sig P -> Y) (y : Y) (V : Ensemble Y) : range f Full_set V -> range (sig_fn_extend f y) P V.
proof: Proof. intros Hf x Hx. cbv. destruct (classic_dec (P x)); try contradiction. apply Hf. constructor. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)