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