Comment by el_pollo_diablo

I am not sure what you mean. Of course proving a new property generally implies reasoning on each elementary step of the program. My point is that, assuming you have already proved a property, proving a new one shouldn't lead you to alter the first proof. But it does if you carelessly use some logical tools like dependent types and single preconditions/postconditions/loop invariants.

For example, take Hoare's while rule (see https://en.wikipedia.org/wiki/Hoare_logic#While_rule). If you have already proved

    {P∧B}S{P}

and, in order to prove another property, some new invariant Q has to be propagated across this loop. It would be enough to prove

    {Q∧B}S{Q}

or even

    {P∧Q∧B}S{Q}

if the new proof builds upon the first one. But if your logical tool of choice insists on having a unique loop invariant, you must throw away your existing proof and prove

    {P∧Q∧B}S{P∧Q}

which is incomparable and uselessly mixes both concerns.