diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-02-23 01:59:36 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-05-28 09:38:36 -0400 |
| commit | dcc77d0dd478b2758d41e35975d31b12e86f61ca (patch) | |
| tree | 16d0593979cf11e401e180a4f7bc9c27798073ec /theories/Init | |
| parent | 4e12d9eb8945120c5cfdb36964fba54dde767b51 (diff) | |
Use extended notation for ex, ex2 types
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Logic.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 35591cbe3..845b8ee9f 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -673,8 +673,8 @@ Section ex. : ex_intro P u1 u2 = ex_intro P v1 v2 := eq_ex u1 v1 u2 v2 p (P_hprop _ _ _). - Lemma rew_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : ex (Q x)) {y} (H : x = y) - : rew [fun a => ex (Q a)] H in u + Lemma rew_ex {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (u : exists p, Q x p) {y} (H : x = y) + : rew [fun a => exists p, Q a p] H in u = match u with | ex_intro _ u1 u2 => ex_intro @@ -723,8 +723,8 @@ Section ex2. Lemma rew_ex2 {A x} {P : A -> Type} (Q : forall a, P a -> Prop) (R : forall a, P a -> Prop) - (u : ex2 (Q x) (R x)) {y} (H : x = y) - : rew [fun a => ex2 (Q a) (R a)] H in u + (u : exists2 p, Q x p & R x p) {y} (H : x = y) + : rew [fun a => exists2 p, Q a p & R a p] H in u = match u with | ex_intro2 _ _ u1 u2 u3 => ex_intro2 |