Theorem keyAssignmentsCompatCompareMajor0 : forall ka kb,
  [] <> keyAssignmentsRemoved ka kb ->
    compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
      = CVersionChangeMajor.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.
