{P : Type} (Psm : X -> Y -> P) (Pl Pr : P) (Pgl : forall a, Psm a pt = Pl) (Pgr : forall b, Psm pt b = Pr) : Smash X Y -> P := Smash_ind Psm Pl Pr (fun x => dp_const (Pgl x)) (fun x => dp_const (Pgr x)).
Require Import Basics.Overture Basics.PathGroupoids Basics.Tactics Basics.Equivalences. Require Import Types.Sum Types.Bool Types.Paths Types.Forall. Require Import WildCat.Core WildCat.Bifunctor WildCat.Equiv. Require Import Colimits.Pushout. Require Import Cubical.DPath. Require Import Pointed.Core.