diff options
| -rwxr-xr-x | theories/Bool/Bool.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 0643ba5404..4b41ca746b 100755 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -541,3 +541,10 @@ Proof. Qed. Hint Resolve bool_1 bool_2 bool_3 bool_4 bool_5 bool_6. + +(** Decidability *) + +Lemma bool_dec : forall a b : bool, {a = b} + { a <> b}. +Proof. + decide equality. +Defined. |