Multiple constructors in deriveComp

[WhatisRT]

We need to deal with branching. We should be able to turn a proof that only at most one constructor applies into an instance of Computational. This means that we'd have to do some proofs by hand, but they should be very easy in practice.