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