proposition: Theorem andb_commutative : forall b c, andb b c = andb c b.
proof: Proof. intros b c. destruct b eqn:Eb. - destruct c eqn:Ec. + reflexivity. + reflexivity. - destruct c eqn:Ec. + reflexivity. + reflexivity. Qed.