Theorem keyAssignmentsCompatCompareMajor1 : forall ka kb k,
  [] = keyAssignmentsRemoved ka kb ->
    (forall f, [] = keyAssignmentsCompatCompareChanged (intersectionPairs f ka kb)) ->
      In k (keyAssignmentsAdded ka kb) ->
        [] <> (keyAssignmentsOverlapping k kb) ->
        compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
          = CVersionChangeMajor.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.
