fact: Definition No_rec_cut (L R : Type@{i}) (s : InSort S L R) (xL : L -> No) (xR : R -> No) (xcut : forall (l:L) (r:R), (xL l) < (xR r)) : No_rec {{ xL | xR // xcut }} = dcut L R _ xL xR xcut (fun l => No_rec (xL l)) (fun r => No_rec (xR r)) (fun l r => No_rec_lt (xL l) (xR r) (xcut l r)) := 1.
imports: HoTT.Basics HoTT.Types TruncType HSet HoTT.Truncations.Core