Conseq derivations and better test for extensions

Factor out the test for extensions that should prevent conseq from breaking
completeness, and refine it. We use to only check for a recipe that is a sum,
now we look for k(_,_+R,_+x) <= ..., k(R,x), ...

Conseq now produces a derivation, which is displayed in the logs. This caused
a little bit of factoring with Tamarin and Maude by the way.