Theorem keyAssignmentsCompatCompareMinor0 : forall ka kb,
  [] = keyAssignmentsRemoved ka kb ->
    (forall f, [] = keyAssignmentsCompatCompareChanged (intersectionPairs f ka kb)) ->
      [] <> (keyAssignmentsAdded ka kb) ->
        Forall (fun j => [] = keyAssignmentsOverlapping j kb) (keyAssignmentsAdded ka kb) ->
          compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
           = CVersionChangeMinor.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.
