proposition: Lemma idtoiso_comp5' (C : PreCategory) (s d d' d'' d''' d'''' : C) (m0 : d''' = d'''') (m1 : d'' = d''') (m2 : d' = d'') (m3 : d = d') (m4 : s = d) : (((idtoiso _ m0 o idtoiso _ m1) o idtoiso _ m2) o idtoiso _ m3) o idtoiso _ m4 = idtoiso _ (m4 @ (m3 @ (m2 @ (m1 @ m0))))%path.
proof: Proof. idtoiso_t. Qed.
imports: Category.Core Functor.Core HoTT.Tactics Basics.Trunc Basics.Tactics Types.Sigma Equivalences