a1 : ap pushout_assoc_left_rec (pgluell a1) = pusha1 a1. Proof. unfold pgluell. rewrite <- (ap_compose (pushl' (pushr' f1 g1 o f2) g2) pushout_assoc_left_rec). change (ap (Pushout_rec P pushb pushc pusha1) (pglue' f1 g1 a1) = pusha1 a1). apply Pushout_rec_beta_pglue. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.