(s : x0 = x1) (v : ap left s = r) : codeglue6 (to O _ (pushl (s;v))) = let z := (frobnicate r s y1 q11)^-1 v in to O Ocodeleft2c (Ocodeleft2ac (Build_Ocodeleft2a s z.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.