{X Y Z : pType} (f : X $-> Z) (g : Y $-> Z) : ap (wedge_rec f g) wglue = point_eq f @ (point_eq g)^ := Pushout_rec_beta_pglue _ f g _ tt.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.