fact: Definition Pushout_ind_beta_pglue (a:A) : apD Pushout_ind (pglue a) = pusha a := Coeq_ind_beta_cglue P (fun bc => match bc with inl b => pushb b | inr c => pushc c end) pusha a.
imports: Basics Types.Paths Types.Arrow Types.Sigma Types.Sum Types.Universe Colimits.Coeq