proposition: Proposition rwhisker_square_comp {w x y z : B} {h₁ : w --> x} {h₂ : y --> z} {v₁ : w -|-> y} {v₂ v₂' v₂'' : x -|-> z} (τ₁ : v₂ =|=> v₂') (τ₂ : v₂' =|=> v₂'') (s : square_double_bicat h₁ h₂ v₁ v₂) : (τ₁ • τ₂) ▹s s = τ₂ ▹s (τ₁ ▹s s).
proof: Proof. exact (pr2 (pr12 (pr12 B)) _ _ _ _ _ _ _ _ _ _ τ₁ τ₂ s). Defined.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat UniMath.Bicategories.Core.Bicat