diff options
Diffstat (limited to 'src/Util/Prod.v')
-rw-r--r-- | src/Util/Prod.v | 5 |
1 files changed, 5 insertions, 0 deletions
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 := |