fact: Definition codeglue4_pushl (s : x0 = x1) (v : ap left s = r) : codeglue4 (to O _ (pushl (s;v))) = to O _ (pushl (pushl (s;v))) := to_O_equiv_natural _ _ _.
imports: HoTT.Basics HoTT.Types Colimits.Pushout Colimits.SpanPushout Homotopy.Join.Core Truncations