From 42b13adb8a512774f2edb8aa0869ac9920c42e43 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 7 Nov 2016 14:30:50 -0500 Subject: Add Proper prod instance --- src/Util/Prod.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/Util/Prod.v') diff --git a/src/Util/Prod.v b/src/Util/Prod.v index b83aea68f..942f0ee99 100644 --- a/src/Util/Prod.v +++ b/src/Util/Prod.v @@ -5,6 +5,7 @@ between two such pairs, or when we want such an equality, we have a systematic way of reducing such equalities to equalities at simpler types. *) +Require Import Coq.Classes.Morphisms. Require Import Crypto.Util.Equality. Require Import Crypto.Util.GlobalSettings. @@ -68,6 +69,10 @@ Section prod. Definition path_prod_ind {A B u v} (P : u = v :> @prod A B -> Prop) := path_prod_rec P. End prod. +Global Instance iff_prod_Proper + : Proper (iff ==> iff ==> iff) (fun A B => prod A B). +Proof. repeat intro; tauto. Defined. + (** ** Useful Tactics *) (** *** [inversion_prod] *) Ltac simpl_proj_pair_in H := -- cgit v1.2.3