{P : Smash X Y -> Type} {Psm : forall a b, P (sm a b)} {Pl : P auxl} {Pr : P auxr} (Pgl : forall a, DPath P (gluel a) (Psm a pt) Pl) (Pgr : forall b, DPath P (gluer b) (Psm pt b) Pr) (a : X) (b : Y) : apD (Smash_ind Psm Pl Pr Pgl Pgr) (glue a b) = ((Pgl a) @Dp ((Pgl pt)^D)) @Dp ((Pgr pt) @Dp ((Pgr b)^D)). Proof. lhs nrapply dp_apD_pp. apply ap011. - apply Smash_ind_beta_gluel'. - apply Smash_ind_beta_gluer'. Defined.
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.