iscontrGuidedHomotopy_comp_2 proved

... after a great deal of struggle.

Advice: for any proof with types more complicated than nat==nat,
avoid "change" and "rewrite".