proposition: Theorem andb_commutative' : forall b c, andb b c = andb c b.
proof: Proof. MProof. intros b c. destruct b. { destruct c. { reflexivity. } { reflexivity. } } { destruct c. { reflexivity. } { reflexivity. } } Qed.