more general Proof_Context.bind_propp, which allows outer parameters; obtain: some support for term bindings within the proof, depending on parameters;