Better support for proving method equivalence

[vkuncak]

The easiest to explain form of strong specification is having two versions of a method and proving that one behaves just like the other (possibly under some joint precondition). The cases include comparing a simple reference method and optimized method, or formally verifying absence of regressions as the code evolves. We should develop methods to make such proofs succeed automatically in as many scenarios as possible.

[vkuncak]

@drganam is adressing this