{A : Type} {D : A -> Type} `{IsD1Cat_Strong A D} {a b c d : A} {f : a $-> b} {g : b $-> c} {h : c $-> d} {a' : D a} {b' : D b} {c' : D c} {d' : D d} (f' : DHom f a' b') (g' : DHom g b' c') (h' : DHom h c' d') : (transport (fun k => DHom k a' d') (cat_assoc_opp_strong f g h) (h' $o' (g' $o' f'))) = (h' $o' g') $o' f'. Proof. apply (moveR_transport_V (fun k => DHom k a' d') (cat_assoc_strong f g h) _ _). exact ((dcat_assoc_strong f' g' h')^). Defined.
Require Import Basics.Overture. Require Import Basics.PathGroupoids. Require Import Basics.Tactics. Require Import Types.Sigma. Require Import WildCat.Core. Require Import WildCat.Prod.