Allow to generate k initial credits in adequacy

This MR adds a parameter k to the adequacy statement to be able to assume k initial later credits in a client proof.