fact: Definition Susp_rec_beta_merid {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.
imports: Basics Types Cubical WildCat Colimits.Pushout NullHomotopy Truncations.Core Modalities.Modality Extensions