Seems like my main problem with proof assistants is that I have to go down to the elementary expressions (with which programmers deal usually) very often, and there is just too many variables to track / keep in mind.
OTOH, maybe it's just the lack of experience, IDK. And I need to learn "surfing" at high level.
@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.
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!