diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-25 14:09:23 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-28 09:38:36 -0400 |
| commit | 179e1d5451411f96a5032e244f2f6cd57463e3bd (patch) | |
| tree | b2c1d17258b3de8d6bd9596aec3cd4fae4cca498 /theories/Init | |
| parent | 745a26bbf47281cbf30ed97cf61c92d4c2ac006c (diff) | |
Use notation for sigT
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. |