{X Y : pType} : ap (@wedge_incl X Y) wglue = 1. Proof. lhs_V nrapply eta_path_prod. lhs nrapply ap011. - lhs_V nrapply ap_compose. nrapply wedge_rec_beta_wglue. - lhs_V nrapply ap_compose. nrapply wedge_rec_beta_wglue. - reflexivity. Defined.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.