Skip to content
Snippets Groups Projects

Add a comment about `cancel_inj` and `cancel_surj`.

Open Robbert Krebbers requested to merge robbert/cancel_inj_surj into master
1 unresolved thread

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
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
Please register or sign in to reply
Loading