Theorem compatVersionChangeMaxComm : forall x y,
  compatVersionChangeMax x y = compatVersionChangeMax y x.
Proof.
  (* Proof omitted for brevity; see Compatibility.v for proofs. *)
Qed.
