proposition: Theorem andb3_exchange : forall b c d, andb (andb b c) d = andb (andb b d) c.
proof: Proof. intros b c d. destruct b eqn:Eb. - destruct c eqn:Ec. { destruct d eqn:Ed. - reflexivity. - reflexivity. } { destruct d eqn:Ed. - reflexivity. - reflexivity. } - destruct c eqn:Ec. { destruct d eqn:Ed. - reflexivity. - reflexivity. } { destruct d eqn:Ed. - reflexivity. - reflexivity. } Qed.