Add static check for `prop_lcsBoth` on coherence of `Both` arguments

[ninioArtillero]

As show by

prop_lcsBoth xs ys = all areMatch $ getDiff xs ys
    where areMatch (Both x y) = x == y
          areMatch _ = True

in the test suite, arguments to Both values produced by getDiff are expected to be equal. This is a consequence of the implementation of getDiffBy, where a local markup makes sure Both values satisfy an equality predicate (such as ==, used by getDiff). This property also holds for getGroupedDiffBy and getGroupedDiff, which are implemented in terms of getDiffBy.

This issue is about writing a Liquid Haskell static check for this property, by specifying a postcondition refining PolyDiff values for the afore mentioned functions. Possibly starting with something like

{-@ reflect coherentDiff @-}
coherentDiff :: (a -> b -> Bool) -> PolyDiff a b -> Bool
coherentDiff eq (Both x y) = eq x y
coherentDiff _ (First _) = True
coherentDiff _ (Second _) = True

{-@ myDiffFunction :: eq (a -> b -> Bool) -> ... -> [ {d : PolyDiff a b | coherentDiff eq d} ] @-}
myDiffFunction :: (a -> b -> Bool) -> ... > [PolyDiff a b]

and then adding supplementary specifications for the check to pass.