{L R : Type} {s : InSort S L R} (xL : L -> GenNo S) (xR : R -> GenNo S) (xcut : forall l r, xL l < xR r) : { rxcut : forall l r, No_raise (xL l) < No_raise (xR r) & No_raise {{ xL | xR // xcut }} = {{ (fun l => No_raise (xL l)) | (fun r => No_raise (xR r)) // rxcut }} }. Proof. eexists. unfold No_raise at 1. rewrite No_rec_cut. reflexivity. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.