`{Funext} (x : No) (xle : x <= x) {L' R' : Type@{i}} {s' : InSort S L' R'} (yL : L' -> No) (yR : R' -> No) (ycut : forall (l:L') (r:R'), (yL l) < (yR r)) (l : L') (p : x = yL l) : x < {{ yL | yR // ycut }}. Proof. generalize dependent x; refine (No_ind_hprop _ _); intros. apply lt_l with l. exact (transport (fun z => {{ xL | xR // xcut}} <= z) p xle). Defined.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.