{x201 x200 x210 x211 : A} {pj01 : x101 = x201} {pj11 : x111 = x211} {pj10 : x110 = x210} {pj00 : x100 = x200} {p2i1 : x201 = x211} {p2i0 : x200 = x210} {p20i : x200 = x201} {p21i : x210 = x211} {sji0 : PathSquare p1i0 p2i0 pj00 pj10} {sji1 : PathSquare p1i1 p2i1 pj01 pj11} {sj0i : PathSquare p10i p20i pj00 pj01} {sj1i : PathSquare p11i p21i pj10 pj11} {s2ii : PathSquare p2i0 p2i1 p20i p21i} (cjii : PathCube s1ii s2ii sji0 sji1 sj0i sj1i) : PathCube s0ii s2ii (sq_concat_h sii0 sji0) (sq_concat_h sii1 sji1) (sq_concat_h si0i sj0i) (sq_concat_h si1i sj1i). Proof. destruct cjii, pi00, pi01, pi10, pi11. exact ciii. Defined.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Types.Paths Types.Prod.