Smash_rec_beta_gluel' {P : Type} {Psm : X -> Y -> P} {Pl Pr : P} (Pgl : forall a, Psm a pt = Pl) (Pgr : forall b, Psm pt b = Pr) (a b : X) : ap (Smash_rec Psm Pl Pr Pgl Pgr) (gluel' a b) = Pgl a @ (Pgl b)^. Proof. lhs nrapply ap_pp. f_ap. 1: apply Smash_rec_beta_gluel. lhs nrapply ap_V. apply inverse2. apply Smash_rec_beta_gluel. 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.