There aren't enough reusable abstractions. I think it's a combination of 1: the ecosystem is too small by lack of manpower and 2: we still don't know how to build interfaces in a way that works well with proofs; typeclasses vs canonical structures is an ongoing debate.
@lyxia As a rule of thumb, I try to match the depth of destruction and construction, and do the reduction and expansion consistently, in particular, unfold the definitions in * |- *, so the level of consideration is "even" across all the premises and conclusions.
I am actually wondering if #SSReflect could help with that, but frankly I doubt it.
Welcome to your niu world ! We are a cute and loving international community Ｏ(≧▽≦)Ｏ !