@andrejbauer Why is that?  The reason that I like proofs like this is that they highlight the main parts of the proof (that it uses `eta_path_sigma`, `allpath_hprop`, and is otherwise done by destructing pairs and substituting equalities, and so there's nothing too deep going on.  I find longer step-by-step proofs tend to be more fragile in the face of refactoring, and also don't actually help me at all unless I'm stepping through them; it's hard to see which lines are just plumbing, and which lines are main ideas, and where order is essential versus where ordering is just because it happened to be that way.