Theorem clipsCompatCompareMajor0 : forall ca cb,
  [] <> clipsRemoved ca cb ->
    compatVersionChangeRecordsMaximum (clipsCompatCompareFull ca cb)
      = CVersionChangeMajor.
Proof.
  (* Proof omitted for brevity; see Clip.v for proofs. *)
Qed.
