Yeah, I guess I can fix this easily by using qed instead of wip in the templates, but I have to check if the error messages will persist, I believe the qed error suppress the helpful messages now.

But this does not scale, there is a lot of copy and paste when the proofs require case analysis, I want to check if I can emit edit comands to the editor in a sane way to automate that copy and pasting.