proposition: Lemma wedge_pr1_inr {X Y} : wedge_pr1 $o (@wedge_inr X Y) $== pconst.
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 pmap_idmap pconst)^). Defined.
imports: Basics Types Pointed.Core Pointed.pSusp Colimits.Pushout WildCat Homotopy.Suspension