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