{X Y : Type} {H_N H_S : Y} {H_merid : X -> H_N = H_S} (x:X) : ap (Susp_rec H_N H_S H_merid) (merid x) = H_merid x. Proof. srapply Pushout_rec_beta_pglue. Defined.
Require Import Basics. Require Import Types. Require Import Cubical.DPath Cubical.DPathSquare. Require Import WildCat. Require Import Colimits.Pushout. Require Import NullHomotopy. Require Import Truncations.Core. Require Import Modalities.Modality. Require Import Extensions.