Think about Curry Howard isomorphism which says programs are proofs and data-types are theorems. A lemma is then like sub-routine. If there is something wrong

Think about Curry Howard isomorphism which says programs are proofs and data-types are theorems. A lemma is then like sub-routine. If there is something wrong in the sub-routine it can often be fixed without requiring any changes to the callers of the sub-routine. It might be the case that the subroutine can never produce a value needed by its callers without changing the types of arguments fed to it, and in such a case it is not enough to fix the subroutine. But in many cases just the lemma-subroutine needs to be corrected, and the rest of the program, rest of the proof can be used as is. https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...