diff --git a/stdpp/base.v b/stdpp/base.v index 210ebad0e0dfe45467a2b2ace971a23f69d8d5c8..e6fb1b49051babfcc46f394a4ec1663073d76488 100644 --- a/stdpp/base.v +++ b/stdpp/base.v @@ -476,6 +476,10 @@ Proof. repeat intro; edestruct (inj2 f); eauto. Qed. Global Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 f} x : Inj R2 R3 (f x). Proof. repeat intro; edestruct (inj2 f); eauto. Qed. +(** Smart constructors for [Inj] and [Surj] based on [Cancel]. These are not +instances because they will blow-up the search space, i.e., in every node of +the search tree for [Inj] or [Surj] of composed functions these instances could +be applied. *) Lemma cancel_inj `{Cancel A B R1 f g, !Equivalence R1, !Proper (R2 ==> R1) f} : Inj R1 R2 g. Proof.