diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 9055437c24..2f36b8bb59 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -303,7 +303,7 @@ Lemma eq_rect_eq : Proof M.eq_rect_eq U. Lemma eq_rec_eq : - forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rect p Q x p h. + forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rec p Q x p h. Proof (fun p Q => M.eq_rect_eq U p Q). (** Injectivity of Dependent Equality *) |