{x x' : X} (p : x = x') : ap (fun t => sm t pt) p = gluel' x x'. Proof. destruct p. symmetry. apply concat_pV. 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.