diff options
Diffstat (limited to 'theories/Bool/IfProp.v')
| -rwxr-xr-x | theories/Bool/IfProp.v | 53 |
1 files changed, 27 insertions, 26 deletions
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 48180678f7..bde404cf75 100755 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -8,42 +8,43 @@ (*i $Id$ i*) -Require Bool. +Require Import Bool. -Inductive IfProp [A,B:Prop] : bool-> Prop - := Iftrue : A -> (IfProp A B true) - | Iffalse : B -> (IfProp A B false). +Inductive IfProp (A B:Prop) : bool -> Prop := + | Iftrue : A -> IfProp A B true + | Iffalse : B -> IfProp A B false. -Hints Resolve Iftrue Iffalse : bool v62. +Hint Resolve Iftrue Iffalse: bool v62. -Lemma Iftrue_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=true -> A. -NewDestruct 1; Intros; Auto with bool. -Case diff_true_false; Auto with bool. +Lemma Iftrue_inv : forall (A B:Prop) (b:bool), IfProp A B b -> b = true -> A. +destruct 1; intros; auto with bool. +case diff_true_false; auto with bool. Qed. -Lemma Iffalse_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=false -> B. -NewDestruct 1; Intros; Auto with bool. -Case diff_true_false; Trivial with bool. +Lemma Iffalse_inv : + forall (A B:Prop) (b:bool), IfProp A B b -> b = false -> B. +destruct 1; intros; auto with bool. +case diff_true_false; trivial with bool. Qed. -Lemma IfProp_true : (A,B:Prop)(IfProp A B true) -> A. -Intros. -Inversion H. -Assumption. +Lemma IfProp_true : forall A B:Prop, IfProp A B true -> A. +intros. +inversion H. +assumption. Qed. -Lemma IfProp_false : (A,B:Prop)(IfProp A B false) -> B. -Intros. -Inversion H. -Assumption. +Lemma IfProp_false : forall A B:Prop, IfProp A B false -> B. +intros. +inversion H. +assumption. Qed. -Lemma IfProp_or : (A,B:Prop)(b:bool)(IfProp A B b) -> A\/B. -NewDestruct 1; Auto with bool. +Lemma IfProp_or : forall (A B:Prop) (b:bool), IfProp A B b -> A \/ B. +destruct 1; auto with bool. Qed. -Lemma IfProp_sum : (A,B:Prop)(b:bool)(IfProp A B b) -> {A}+{B}. -NewDestruct b; Intro H. -Left; Inversion H; Auto with bool. -Right; Inversion H; Auto with bool. -Qed. +Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}. +destruct b; intro H. +left; inversion H; auto with bool. +right; inversion H; auto with bool. +Qed.
\ No newline at end of file |