This issue seems hallucinated. In the real world we just update our proofs. https://sos-vo.org/node/69931

How hypocritical of someone preaching the virtues of formal proofs to be using a single example to try to prove the 'for all' case... As if it's feasible for all systems, for all requirements, under all possible financial constraints.

Oh yes, I'm the LLM here.

Maybe you should run your comments through your Coq proof-assistant before you post them!