{X : pType} (x : X) : ap (psusp_pinch X) (merid x) = ap wedge_inl (loop_susp_unit X x) @ wglue @ ap wedge_inr (loop_susp_unit X x) @ wglue^. Proof. rapply Susp_rec_beta_merid. Defined.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.