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