diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-22 18:21:49 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-22 18:21:49 -0400 |
| commit | 345a6839f50ced938b615298e926d01e4e169a0e (patch) | |
| tree | fdc997d0d751f98e26a244ad97c1dc6e30145b85 /src/Specific/IntegrationTestTemporaryMiscCommon.v | |
| parent | 5bdf938896c4bb1baab793daaeaf0bfa418d8d9e (diff) | |
Add sig_conj_by_impl2
Diffstat (limited to 'src/Specific/IntegrationTestTemporaryMiscCommon.v')
| -rw-r--r-- | src/Specific/IntegrationTestTemporaryMiscCommon.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Specific/IntegrationTestTemporaryMiscCommon.v b/src/Specific/IntegrationTestTemporaryMiscCommon.v index ab1e821d6..4e012486c 100644 --- a/src/Specific/IntegrationTestTemporaryMiscCommon.v +++ b/src/Specific/IntegrationTestTemporaryMiscCommon.v @@ -74,3 +74,7 @@ Ltac eexists_sig_etransitivity_for_rewrite_fun := => let lem := open_constr:(@sig_eq_trans_rewrite_fun_exist1 A _ f _ b) in simple refine (lem _ _); cbv beta end. +Definition sig_conj_by_impl2 {A} {P Q : A -> Prop} (H : forall a : A, Q a -> P a) + (H' : { a : A | Q a }) + : { a : A | P a /\ Q a } + := let (a, p) := H' in exist _ a (conj (H a p) p). |