Add a comment about `cancel_inj` and `cancel_surj`.
1 unresolved thread
1 unresolved thread
Merge request reports
Activity
Filter activity
476 476 Global Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 f} x : Inj R2 R3 (f x). 477 477 Proof. repeat intro; edestruct (inj2 f); eauto. Qed. 478 478 479 (** Smart constructors for [Inj] and [Surj] based on [Cancel]. These are not Just apply them to your
Inj
orSurj
goal, see !529 (merged) for an example.
Please register or sign in to reply