{P : Type} {Psm : X -> Y -> P} {Pl Pr : P} (Pgl : forall a, Psm a pt = Pl) (Pgr : forall b, Psm pt b = Pr) (b : Y) : ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluer b) = Pgr b. Proof. rhs_V nrapply (eissect dp_const). apply moveL_equiv_V. lhs_V nrapply dp_apD_const. nrapply 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.