a2 : ap pushout_assoc_left_rec (pgluelr a2) = pusha2 a2. Proof. unfold pushout_assoc_left_rec, pgluelr. apply (Pushout_rec_beta_pglue (f := pushr' f1 g1 o f2) (g := g2)). Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.