[Lean] Custom purification proofs for for-loops

[abentkamp]

#1951 has hard-coded the purification proof for the loop invariant for for-loops. This should be adapted depending on the selected proof method, and it should be customizable by the user with an additional attribute.

Related issue: #1783