aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Equality.v
diff options
context:
space:
mode:
authorJason Gross <jgross@mit.edu>2018-09-14 21:16:12 -0400
committerJason Gross <jgross@mit.edu>2018-09-14 21:16:12 -0400
commitb98ec63895887435aa6f08436715200d33a62d98 (patch)
treec605dc8fe8656a628e5fa4edf097d972f7fbfd62 /src/Util/Equality.v
parenta3a077040a311f32199c86700a463a5cf661b76a (diff)
Add PrimitiveSigma
Diffstat (limited to 'src/Util/Equality.v')
-rw-r--r--src/Util/Equality.v7
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Util/Equality.v b/src/Util/Equality.v
index 04335dbd4..d1a711821 100644
--- a/src/Util/Equality.v
+++ b/src/Util/Equality.v
@@ -8,6 +8,13 @@ Require Import Coq.Classes.Morphisms.
Require Import Crypto.Util.Isomorphism.
Require Import Crypto.Util.HProp.
+Import EqNotations.
+
+Definition f_equal_dep {A B} (f : forall a : A, B a) (x y : A) (H : x = y) : rew [B] H in f x = f y
+ := match H with
+ | eq_refl => eq_refl
+ end.
+
(** Most of the structure of proofs of equalities fits into what
mathematicians call a weak ∞-groupoid. (In fact, one way of
*defining* a weak ∞-groupoid is via what's called the J-rule,