{A B : Type} (u v z w : A * B) (p : fst u = fst v) (q : fst v = fst z) (r : fst z = fst w) (p' : snd u = snd v) (q' : snd v = snd z) (r' : snd z = snd w) : path_prod_pp u z w (p @ q) r (p' @ q') r' @ whiskerR (path_prod_pp u v z p q p' q') (path_prod z w r r') @ concat_pp_p (path_prod u v p p') (path_prod v z q q') (path_prod z w r r') = ap011 (path_prod u w) (concat_pp_p p q r) (concat_pp_p p' q' r') @ path_prod_pp u v w p (q @ r) p' (q' @ r') @ whiskerL (path_prod u v p p') (path_prod_pp v z w q r q' r'). Proof. destruct u, v, z, w; simpl in *; destruct p, p', q, q', r, r'. reflexivity. Defined.
Require Import Basics.Overture Basics.Equivalences Basics.PathGroupoids Require Import Types.Empty.