proposition: Lemma Conway_theorem0_lemma1 `{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: 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.
imports: HoTT.Basics HoTT.Types TruncType HSet HoTT.Truncations.Core