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