Reflective reasoning with and between a declarative metatheory and the implementation code