fact: Definition commute_homotopy_id {A} {f : A -> A} (H : forall a, f a = a) {x y : A} (p : x = y) : eq_trans (H x) p = eq_trans (f_equal f p) (H y) := match p in (_ = y) return eq_trans (H x) p = eq_trans (f_equal f p) (H y) with eq_refl => eq_sym (eq_trans_refl_l (H x)) end.