proposition: Lemma BoolTheory : ring_theory false true xorb andb xorb (fun b:bool => b) (eq(A:=bool)).
proof: Proof. split; simpl. - intros x; destruct x; reflexivity. - intros x y; destruct x; destruct y; reflexivity. - intros x y z; destruct x; destruct y; destruct z; reflexivity. - reflexivity. - intros x y; destruct x; destruct y; reflexivity. - intros x y; destruct x; destruct y; reflexivity. - intros x y z; destruct x; destruct y; destruct z; reflexivity. - reflexivity. - intros x; destruct x; reflexivity. Qed.
imports: Bool Ring_theory Ring_base InitialRing Ring_tac