"It is written once and not maintained..." Be careful, this is how you get the Ariane V first flight. "You do not need to understand the lammas coq uses to he

"It is written once and not maintained..." Be careful, this is how you get the Ariane V first flight. "You do not need to understand the lammas coq uses to help you prove your theorem..." If I wanted to generalize your theorem or move it to some other base abstraction, the first thing I need to do is to read and understand your proof. If that proof is made up of Coq tactics chosen based on "whatever works", I'm going to have a bad day. Now, many results especially in CS are made by reducing a new problem to an existing theorem, but I don't know how well that works as a general case.