(L R : Type@{i}) (s : InSort S L R) (xL : L -> GenNo) (xR : R -> GenNo) (xcut : forall (l:L) (r:R), (xL l) < (xR r)) : No_ind {{ xL | xR // xcut }} = dcut L R _ xL xR xcut (fun l => No_ind (xL l)) (fun r => No_ind (xR r)) (fun l r => No_ind_lt (xL l) (xR r) (xcut l r)) := 1.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.