diff options
Diffstat (limited to 'theories/Bool/IfProp.v')
| -rw-r--r-- | theories/Bool/IfProp.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 7e9087c377..8366e8257e 100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -29,13 +29,13 @@ case diff_true_false; trivial with bool. Qed. Lemma IfProp_true : forall A B:Prop, IfProp A B true -> A. -intros. +intros A B H. inversion H. assumption. Qed. Lemma IfProp_false : forall A B:Prop, IfProp A B false -> B. -intros. +intros A B H. inversion H. assumption. Qed. @@ -45,7 +45,7 @@ destruct 1; auto with bool. Qed. Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}. -destruct b; intro H. +intros A B b; destruct b; intro H. - left; inversion H; auto with bool. - right; inversion H; auto with bool. Qed. |