Metatheoretical Work

[VictorCMiraldo]

There is a number of things that require attention on the metatheoretical level.

First and foremost, definition of \subseteq for patches, secondly, thin operator.
Then, we'd like to know whether they are related or not. Hopefully, this informs us enough to
know whether copies closer to the root are better than more copies further down the tree with contractions.

diff (Bin (Bin t k) u) (Bin (Bin t k) t)

[VictorCMiraldo]

From the merging experiments, copies closer to the root yield more mergeable patches.

Quickcheck tells me composition should really be associative, but I've been struggling to produce a proof lately.