proposition: Lemma sig_fn_extend_injective_ens {X Y : Type} {P : X -> Prop} (f : sig P -> Y) (y : Y) : injective_ens (sig_fn_extend f y) P <-> injective f.
proof: Proof. split. - intros Hf [x0 Hx0] [x1 Hx1] Hx. specialize (Hf x0 x1 Hx0 Hx1). apply subset_eq_compat. apply Hf. clear Hf. cbv. destruct (classic_dec _), (classic_dec _); try contradiction. destruct (proof_irrelevance _ Hx0 p). destruct (proof_irrelevance _ Hx1 p0). assumption. - intros Hf x0 x1 Hx0 Hx1 Hx. specialize (Hf (exist P x0 Hx0) (exist P x1 Hx1)). cbv in Hx. destruct (classic_dec _), (classic_dec _); try contradiction. destruct (proof_irrelevance _ Hx0 p). destruct (proof_irrelevance _ Hx1 p0). specialize (Hf Hx). inversion Hf; subst; clear Hf. reflexivity. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)