diff options
| -rw-r--r-- | theories/Bool/BoolEq.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Bool/BoolEq.v b/theories/Bool/BoolEq.v index f002ee427c..dd10c758a5 100644 --- a/theories/Bool/BoolEq.v +++ b/theories/Bool/BoolEq.v @@ -46,7 +46,7 @@ Section Bool_eq_dec. Definition exists_beq_eq : forall x y:A, {b : bool | b = beq x y}. Proof. - intros. + intros x y. exists (beq x y). constructor. Defined. |