diff options
| author |  Jason Gross <jagro@google.com> | 2018-08-13 23:58:49 -0400 |
|---|---|---|
| committer |  Jason Gross <jgross@mit.edu> | 2018-08-15 22:09:50 -0400 |
| commit | 8926b3f6b2aa1fe0f8d3f65f1966f60402cad4b9 (patch) | |
| tree | b4f92732531a3aab686f2e4a5a9f98d4264e61b0 /src/Util/Bool.v | |
| parent | f4d27f9218990b904da65ec4e87ed5d84358ce65 (diff) | |
Prove monotonicity properties about zrange
Diffstat (limited to 'src/Util/Bool.v')
| -rw-r--r-- | src/Util/Bool.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/Util/Bool.v b/src/Util/Bool.v index fe6ae64e4..fb2038de5 100644 --- a/src/Util/Bool.v +++ b/src/Util/Bool.v @@ -103,3 +103,8 @@ Ltac split_andb_in_context := repeat split_andb_in_context_step. Lemma if_const A (b : bool) (x : A) : (if b then x else x) = x. Proof. case b; reflexivity. Qed. + +Lemma ex_bool_iff_or P : @ex bool P <-> (or (P true) (P false)). +Proof. + split; [ intros [ [] ? ] | intros [?|?]; eexists ]; eauto. +Qed. |