proposition: Lemma partial_injection_preord: preorder partial_injection_ord.
proof: Proof. constructor. red; intros. destruct x. constructor. auto with sets. intros. 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: FunctionProperties Relation_Definitions Relation_Definitions_Implicit CSB EnsemblesSpec ClassicalChoice ZornsLemma EnsemblesImplicit ProofIrrelevance FunctionalExtensionality Description