{f12'' : x02 = x} {f12' : x22 = x} : PathSquare f10 (f12'' @ f12'^) f01 f21 <~> PathSquare f10 f12'' f01 (f21 @ f12'). Proof. clear f12. destruct f12'. refine (sq_cccG (concat_p1 _)^ oE _). refine (sq_cGcc (concat_p1 _)). Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.