for precondition checker, write composiing checker function and compose soundness proofs into one theorem