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.