diff options
Diffstat (limited to 'src/Util/Prod.v')
| -rw-r--r-- | src/Util/Prod.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/Prod.v b/src/Util/Prod.v index bcd9404a6..6e6c7d3c4 100644 --- a/src/Util/Prod.v +++ b/src/Util/Prod.v @@ -16,6 +16,10 @@ Local Arguments f_equal {_ _} _ {_ _} _. Scheme Equality for prod. +Definition fst_pair {A B} (a:A) (b:B) : fst (a,b) = a := eq_refl. +Definition snd_pair {A B} (a:A) (b:B) : snd (a,b) = b := eq_refl. +Create HintDb cancel_pair discriminated. Hint Rewrite @fst_pair @snd_pair : cancel_pair. + (** ** Equality for [prod] *) Section prod. (** *** Projecting an equality of a pair to equality of the first components *) |