Add missing clause to 'patchL'

It is present in the thesis' Agda version but
also dropped in the Haskell version, which was
the basis for the 'gdiff' library.

As explained in the thesis, patchL is not total
but this clause was strictly necessary to work
at all.