proposition: Lemma partial_injection_preord: preorder partial_injection_ord.
proof: Proof. constructor. - red; intros. destruct x. constructor. + auto with sets. + intros. simpl in *. assert (i1 = i2). { apply proof_irrelevance. } rewrite H. reflexivity. - red; intros. destruct H. destruct H0. constructor. + auto with sets. + intros. assert (In (pi_dom y) x0). { auto with sets. } transitivity (pi_func y x0 H); trivial. Qed.
imports: Coq(ClassicalChoice) Coq(ProofIrrelevance) Coq(FunctionalExtensionality) Coq(Description) ZornsLemma(FunctionPropertiesEns) ZornsLemma(Relation_Definitions_Implicit) ZornsLemma(CSB) ZornsLemma(EnsemblesSpec) ZornsLemma(ZornsLemma) ZornsLemma(EnsemblesImplicit) ZornsLemma(CountableTypes) ZornsLemma(FiniteTypes) ZornsLemma(InfiniteTypes) Coq(RelationClasses)