equiv_cu_GGGGGG t0ii t1ii tii0 tii1 1 1.
Require Import Basics. Require Import Cubical.DPath. Require Import Cubical.PathSquare. Require Import Cubical.DPathSquare. Require Import Types.Paths Types.Prod.