{qx1 : DPath P px1 b01 b11} {q0x : DPath P p0x b00 b01} {q1x : DPath P p1x b10 b11} {qx0 : DPath P px0 b00 b10} (t : DPathSquare P s qx0 qx1 q0x q1x) {qx0' : DPath P px0 b00 b10} (t' : DPathSquare P s qx0' qx1 q0x q1x) : qx0 = qx0'. Proof. destruct s. exact (sq_fill_l_uniq t t'). Defined.
Require Import Basics. Require Import Types.Paths. Require Import Cubical.DPath. Require Import Cubical.PathSquare.