fact: Definition No_rec_lt (x y : No) (p : x < y) : dlt (No_rec x) (No_rec y) := No_ind_lt (fun _ => A) (fun _ _ _ a b => dle a b) (fun _ _ _ a b => dlt a b) _ _ _ _ _ x y p.
imports: HoTT.Basics HoTT.Types TruncType HSet HoTT.Truncations.Core