{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)) : GenNo := Build_No (opt (game_of o xL) (game_of o xR)) (isno _ _ _ _ _ (isno_game_of o xL) (isno_game_of o xR) xcut).
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.