pushout_assoc_left -> P. Proof. srefine (Pushout_rec _ _ pushd _). - srefine (Pushout_rec _ pushb pushc pusha1). - exact pusha2. Defined.
Require Import Basics. Require Import Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe.