Module Proof_encoding.V2