fact: Definition nullhomot_paths_from_susp {X Z : Type} (H_N H_S : Z) (f : X -> H_N = H_S) (n : NullHomotopy (Susp_rec H_N H_S f)) : NullHomotopy f.
imports: Basics Types Cubical WildCat Colimits.Pushout NullHomotopy Truncations.Core Modalities.Modality Extensions