provide first version of BackchainingLib

This lib is used to combine matching preconditions against assumptions
in the goalstack with conditional rewriting. This enables efficient
backwards-chaining with theorems like

``!x y. R x y ==> !x' y'. complicated condition ==> R x' y'``