proposition: Lemma p_composition_of_coherent_iso_for_rewrite__isisomorphism_helper' : @IsIsomorphism (_ -> _) _ _ (n2 ^-1 o (f2 oL n1 ^-1 o (associator_1 f2 f1 f3 o (n0 oR f3 o n))))%natural_transformation.
proof: Proof. eapply isisomorphism_compose; [ eapply isisomorphism_inverse | eapply isisomorphism_compose; [ eapply iso_whisker_l; eapply isisomorphism_inverse | eapply isisomorphism_compose; [ typeclasses eauto | eapply isisomorphism_compose; [ eapply iso_whisker_r; typeclasses eauto | typeclasses eauto ] ] ] ]. Defined.
imports: Category.Core Functor.Core NaturalTransformation.Core Category.Morphisms FunctorCategory.Morphisms Functor.Composition.Core NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws NaturalTransformation.Isomorphisms NaturalTransformation.Paths FunctorCategory.Core Pseudofunctor.Core HoTT.Tactics