(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.2                                 *)
(*                               May 1st 1998                               *)
(*                                                                          *)
(****************************************************************************)
(*                                  IfProp.v                                *)
(****************************************************************************)

Require Bool.

Inductive IfProp [A,B:Prop] : bool-> Prop 
  := Iftrue  : A -> (IfProp A B true)
  |  Iffalse : B -> (IfProp A B false).

Hint Iftrue Iffalse.

Lemma Iftrue_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=true -> A.
Destruct 1; Intros; Auto.
Case diff_true_false; Auto.
Save.

Lemma Iffalse_inv : (A,B:Prop)(b:bool) (IfProp A B b) -> b=false -> B.
Destruct 1; Intros; Auto.
Case diff_true_false; Trivial.
Save.

Lemma IfProp_or : (A,B:Prop)(b:bool)(IfProp A B b) -> A\/B.
Destruct 1; Auto.
Save.

Lemma IfProp_sum : (A,B:Prop)(b:bool)(IfProp A B b) -> {A}+{B}.
Destruct b; Intro H.
Left; Inversion H; Auto.
Right; Inversion H; Auto.
Save.

(* $Id: IfProp.v,v 1.5 1998/04/30 16:45:45 mohring Exp $ *)
