(s : x0 = x1) (v : ap left s = r) : codeglue3 (to O _ (pushl (to O _ (s;v)))) = to O _ (pushl (s;v)) := inverse_equiv_O_pushout_to_O_pushl _ _ _ _.
Require Import HoTT.Basics HoTT.Types. Require Import Colimits.Pushout. Require Import Colimits.SpanPushout. Require Import Homotopy.Join.Core. Require Import Truncations.