diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-04-20 13:59:33 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-04-20 13:59:33 -0400 |
| commit | f2629738a4dfd748a4829323959607ee36e6fd6d (patch) | |
| tree | 7ffd7b5aefdef22e34aea54f97367833f3ff3084 /src/Util/CaseUtil.v | |
| parent | b5663bdb42176ac0e808eda16af031c795c22164 (diff) | |
moved lemmas from ModularBaseSystemProofs to various Util files
Diffstat (limited to 'src/Util/CaseUtil.v')
| -rw-r--r-- | src/Util/CaseUtil.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/CaseUtil.v b/src/Util/CaseUtil.v index af04a1e49..cf3ebf29c 100644 --- a/src/Util/CaseUtil.v +++ b/src/Util/CaseUtil.v @@ -10,3 +10,9 @@ Ltac case_max := (exact (le_Sn_le _ _ (not_le _ _ H))) end end. + +Lemma pull_app_if_sumbool {A B X Y} (b : sumbool X Y) (f g : A -> B) (x : A) + : (if b then f x else g x) = (if b then f else g) x. +Proof. + destruct b; reflexivity. +Qed. |