Library mathcomp.ssreflect.ssrfun
From mathcomp Require Import ssreflect.
From Coq Require Export ssrfun.
From mathcomp Require Export ssrnotations.
From Coq Require Export ssrfun.
From mathcomp Require Export ssrnotations.
Local additions:
void == a notation for the Empty_set type of the standard library.
of_void T == the canonical injection void -> T.
Lemma Some_inj {T : nonPropType} : injective (@Some T).
Notation void := Empty_set.
Definition of_void T (x : void) : T := match x with end.
Lemma of_voidK T : pcancel (of_void T) [fun _ ⇒ None].
Lemma inj_compr A B C (f : B → A) (h : C → B) :
injective (f \o h) → injective h.
Definition injective2 (rT aT1 aT2 : Type) (f : aT1 → aT2 → rT) :=
∀ (x1 x2 : aT1) (y1 y2 : aT2), f x1 y1 = f x2 y2 → (x1 = x2) × (y1 = y2).
Arguments injective2 [rT aT1 aT2] f.