@amy I do not like LLMs but I do admit that I love Agda more than I hate LLMs. Perhaps it was naive of me to believe there might be a possible compromise that is at least somewhat acceptable to everyone in the team. But my love for the project forces me to at least try to find a solution - even if as you say it is impossible. If it makes you feel better to be angry with me for trying, then so be it. I'm just tired.