Make shorthand versions of the consequence rule

[joom]

If the new precondition for the consequence rule (in Hoare logic) is the same as the conclusion's precondition, or if the new postcondition for the consequence rule is the same as the conclusion's postcondition, then the one that is the same can be omitted from the premises of the consequence rule as a shorthand notation, since it can be proved with a single identity rule, which is not interesting. For proof compactness, we often omit the uninteresting case when we write proofs.