{X Y : pType} : X \/ Y $-> Y := wedge_rec pconst pmap_idmap.
Require Import Basics Types. Require Import Pointed.Core Pointed.pSusp. Require Import Colimits.Pushout. Require Import WildCat. Require Import Homotopy.Suspension.