diff options
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Specif.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index e4c57c6c1..771a10531 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -265,7 +265,7 @@ Section sigT. but for simplicity, we don't. *) Definition eq_sigT_uncurried_iff {A P} (u v : { a : A & P a }) - : u = v <-> (sigT (fun p : projT1 u = projT1 v => rew p in projT2 u = projT2 v)). + : u = v <-> { p : projT1 u = projT1 v & rew p in projT2 u = projT2 v }. Proof. split; [ intro; subst; exists eq_refl; reflexivity | apply eq_sigT_uncurried ]. Defined. |