proposition: Lemma slices_well_defined: forall (a:A) (b1 b2:B), S b1 b2 -> f a b1 = f a b2.
proof: Proof. intros. apply well_defined_2arg. - apply (equiv_refl equivR). - assumption. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(ImageImplicit) ZornsLemma(Relation_Definitions_Implicit) Coq(Description) Coq(ProofIrrelevance)