From 94e1bf37bbdabe3f2cf300e60a8c4eb856aa4819 Mon Sep 17 00:00:00 2001
From: Christian Doczkal
Date: Thu, 10 Sep 2020 18:30:42 +0200
Subject: new mem_imset lemmas

---
 mathcomp/ssreflect/ssrfun.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'mathcomp/ssreflect/ssrfun.v')

diff --git a/mathcomp/ssreflect/ssrfun.v b/mathcomp/ssreflect/ssrfun.v
index f189dcb..c789e67 100644
--- a/mathcomp/ssreflect/ssrfun.v
+++ b/mathcomp/ssreflect/ssrfun.v
@@ -21,3 +21,8 @@ Proof. by case. Qed.
 Lemma inj_compr A B C (f : B -> A) (h : C -> B) :
    injective (f \o h) -> injective h.
 Proof. by move=> fh_inj x y /(congr1 f) /fh_inj. Qed.
+
+Definition injective2 (rT aT1 aT2 : Type) (f : aT1 -> aT2 -> rT) :=
+  forall (x1 x2 : aT1) (y1 y2 : aT2), f x1 y1 = f x2 y2 -> (x1 = x2) * (y1 = y2).
+
+Arguments injective2 [rT aT1 aT2] f.
-- 
cgit v1.2.3