Many fixes to the proof of lem:func_retract_to_fiber_retract
Errata for b212091, unmarked.
Merge pull request #458 from cangiuli/issue-451

Fix Lemma 4.7.3, closing #451.