@hallasurvivor I make this distinction too

@hallasurvivor walking from here to there (points to easily visible location) is straightforward. walking from here to here (shifts weight to other foot) is trivial.

@hallasurvivor Without any more context, who can judge?

@hallasurvivor Logic isn’t always easy and I would probably have done the same.

@hallasurvivor This is me every time I try to describe what was involved in adapting a proof from ZF to IZF. After "straightforward" comes "a small number of changes", "small changes in many places", "many changes but basically the same proof" &c &c