{A B C} {f : A -> B} {g : A -> C} (P : Type) (pushb : B -> P) (pushc : C -> P) (pusha : forall a : A, pushb (f a) = pushc (g a)) : @Pushout A B C f g -> P := @Coeq_rec _ _ (inl o f) (inr o g) P (sum_rec P pushb pushc) pusha.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.