I think that’s to a certain extent a matter of approach: we’ve discovered over time that certain approaches e.g. huge business logic inheritance trees are susceptible to this problem, whereas others e.g. list comprehensions, grouping constructs, functors &c aren’t.

So I’m sure you _can_ build something in Coq that is fragile as you describe, but I feel sure that there are alternative approaches that won’t be as brittle.