proposition: Lemma wedge_pr2_inr {X Y} : wedge_pr2 $o (@wedge_inr X Y) $== pmap_idmap.
proof: Proof. snrapply Build_pHomotopy. 1: reflexivity. rhs nrapply concat_p1. rhs nrapply concat_p1. rhs nrapply (ap_V _ wglue). exact (inverse2 (wedge_rec_beta_wglue pconst pmap_idmap)^). Defined.
imports: Basics Types Pointed.Core Pointed.pSusp Colimits.Pushout WildCat Homotopy.Suspension