diff options
| -rw-r--r-- | theories/Bool/DecBool.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Bool/DecBool.v b/theories/Bool/DecBool.v index ef78121d63..5eb2a99739 100644 --- a/theories/Bool/DecBool.v +++ b/theories/Bool/DecBool.v @@ -18,7 +18,7 @@ Theorem ifdec_left : forall (A B:Prop) (C:Set) (H:{A} + {B}), ~ B -> forall x y:C, ifdec H x y = x. Proof. - intros; case H; auto. + intros A B C H **; case H; auto. intro; absurd B; trivial. Qed. @@ -26,7 +26,7 @@ Theorem ifdec_right : forall (A B:Prop) (C:Set) (H:{A} + {B}), ~ A -> forall x y:C, ifdec H x y = y. Proof. - intros; case H; auto. + intros A B C H **; case H; auto. intro; absurd A; trivial. Qed. |