sq_concat_h s hr = sq_ccGG (concat_p1 _)^ (concat_p1 _)^ s. Proof. by destruct s. Defined.
Require Import Basics. Require Import Types.Paths Types.Prod. Require Import DPath. Section PathSquaresFromPaths. End PathSquaresFromPaths.