{X Y} : wedge_pr2 $o (@wedge_inl X Y) $== pconst. Proof. reflexivity. Defined.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.