{A B C f g} (P : Type) (pushb : B -> P) (pushc : C -> P) (pusha : forall a : A, pushb (f a) = pushc (g a)) (a : A) : ap (Pushout_rec P pushb pushc pusha) (pglue a) = pusha a. Proof. nrapply Coeq_rec_beta_cglue. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.