a1 : ap pushout_assoc_right_rec (pgluerl a1) = pusha1 a1. Proof. unfold pushout_assoc_right_rec, pgluerl. apply (Pushout_rec_beta_pglue (f := f1) (g := pushl' f2 g2 o g1)). Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.