(R : SPushout -> Type) (spushl' : forall x, R (spushl x)) (spushr' : forall y, R (spushr y)) (sglue' : forall x y (q : Q x y), transport R (spglue q) (spushl' x) = (spushr' y)) : forall p, R p. Proof. srapply (@Pushout_ind {xy:X * Y & Q (fst xy) (snd xy)} X Y (fst o pr1) (snd o pr1) R spushl' spushr'). intros [[x y] q]; cbn in *. apply sglue'; assumption. Defined.
Require Import HoTT.Basics HoTT.Colimits.Pushout.