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