Definition bool_not (b:bool) := if b then false else true. Definition bool_eq (b1:bool)(b2:bool) := if b1 then b2 else bool_not b2. Definition bool_xor (b1:bool)(b2:bool) := bool_not (bool_eq b1 b2). Definition bool_and (b1:bool)(b2:bool) := if b1 then b2 else false. Definition bool_or (b1:bool)(b2:bool) := if b1 then true else b2. Theorem first : forall b1 b2 :bool, bool_xor b1 b2 = bool_not (bool_eq b1 b2). auto. Qed. Theorem second : forall b1 b2 :bool, bool_not (bool_and b1 b2) = bool_or (bool_not b1) (bool_not b2). induction b1; auto. Qed. Theorem third : forall b :bool, bool_not (bool_not b) = b. induction b; auto. Qed. Theorem fourth : forall b :bool, bool_or b (bool_not b) = true. induction b; auto. Qed. Theorem fifth : forall b1 b2:bool, bool_eq b1 b2 = true -> b1 = b2. induction b1; auto. induction b2; auto. Qed. Theorem sixth : forall b1 b2 :bool, b1 = b2 -> bool_eq b1 b2 = true. induction b1; auto. induction b2; auto. Qed. Theorem seventh : forall b1 b2:bool, bool_not (bool_or b1 b2) = bool_and (bool_not b1) (bool_not b2). induction b1; auto. Qed. Theorem eighth : forall b1 b2 b3:bool, bool_or(bool_and b1 b3) (bool_and b2 b3) = bool_and(bool_or b1 b2) b3. induction b1; auto. induction b3; auto. induction b2; auto. Qed.