equiv_cu_GGGGGG 1 1 tii0 tii1 ti0i ti1i.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Types.Paths Types.Prod.