1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: IfProp.v 8642 2006-03-17 10:09:02Z notin $ i*)
13
Inductive IfProp (A B:Prop) : bool -> Prop :=
14
| Iftrue : A -> IfProp A B true
15
| Iffalse : B -> IfProp A B false.
17
Hint Resolve Iftrue Iffalse: bool v62.
19
Lemma Iftrue_inv : forall (A B:Prop) (b:bool), IfProp A B b -> b = true -> A.
20
destruct 1; intros; auto with bool.
21
case diff_true_false; auto with bool.
25
forall (A B:Prop) (b:bool), IfProp A B b -> b = false -> B.
26
destruct 1; intros; auto with bool.
27
case diff_true_false; trivial with bool.
30
Lemma IfProp_true : forall A B:Prop, IfProp A B true -> A.
36
Lemma IfProp_false : forall A B:Prop, IfProp A B false -> B.
42
Lemma IfProp_or : forall (A B:Prop) (b:bool), IfProp A B b -> A \/ B.
43
destruct 1; auto with bool.
46
Lemma IfProp_sum : forall (A B:Prop) (b:bool), IfProp A B b -> {A} + {B}.
48
left; inversion H; auto with bool.
49
right; inversion H; auto with bool.
b'\\ No newline at end of file'