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