{A} {a00 a10 a01 a11 : A} {px0 : a00 = a10} {px1 : a01 = a11} {p0x : a00 = a01} {p1x : a10 = a11} {s s' : PathSquare px0 px1 p0x p1x} : s = s' <~> PathCube hr hr s s' vr vr. Proof. refine (cu_rot_tb_fb oE _). refine (cu_rot_tb_fb oE _). refine (cu_ccGGGG _ _ _ _ oE _). 1,2: exact sq_tr_refl_v^. 1,2: exact (eisretr tr _)^. refine (_ oE equiv_ap' tr _ _). apply equiv_cu_G11. Defined.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Types.Paths Types.Prod.