Require Bool.

Lemma bool_dec1
     : (b:bool)~(Is_true b)->(Is_true (negb b)).

Lemma bool_dec2
     : (b:bool)~b=true->(Is_true (negb b)).

Lemma bool_dec3
     : (b:bool)(Is_true b)->(b=true).

Lemma bool_dec4
     : (b:bool)~b=false->b=true.

Lemma bool_dec5
     : (b:bool)~b=true->b=false.

Lemma bool_dec6
     : (b:bool)b=false->~b=true.

Lemma bool_dec7
     : (b:bool)b=true->~b=false.

Section boolean_extension.

(* Giving if constructor over bool for general sets.*)

Hypothesis genset:Set.
Recursive Definition
    Setifb : bool->genset->genset->genset :=
	true x y => x |
	false x y => y.

Lemma orbor : (b1,b2:bool)
	(orb b1 b2)=true->b1=true\/b2=true.

End boolean_extension.

Lemma ororb : (b1,b2:bool)
	(b1=true\/b2=true)->(orb b1 b2)=true.

Lemma orbor1 :  (b1,b2:bool)
	(orb b1 b2)=false->b1=false/\b2=false.

Lemma ororb1 : (b1,b2:bool)
	(b1=false/\b2=false)->(orb b1 b2)=false.

Lemma sym_andb : (b1,b2:bool)
	(andb b1 b2)=(andb b2 b1).

Lemma andbf : (b:bool)
	(andb b false)=false.