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