{L' R' : Type@{i} } {Sy : InSort S L' R'} (yL : L' -> No) (yR : R' -> No) (ycut : forall (l : L') (r : R'), yL l < yR r) : let L'' := L + L' in let R'' := R + R' in let zL := sum_ind (fun _ => No) (fun l => (xL_plus l).1 {{ yL | yR // ycut }}) (fun l => (plus_inner.1 (yL l)).1) : L'' -> No in let zR := sum_ind (fun _ => No) (fun r => (xR_plus r).1 {{ yL | yR // ycut }}) (fun r => (plus_inner.1 (yR r)).1) : R'' -> No in let Sz := sum_options L R L' R' _ _ in { zcut : forall (l:L'') (r:R''), zL l < zR r & (plus_inner.1 {{ yL | yR // ycut }}).1 = (@No_cut _ _ _ Sz zL zR zcut) }. Proof. eexists. rel_hnf. reflexivity. Qed.
Require Import HoTT.Basics HoTT.Types. Require Import HoTT.Spaces.No.Core HoTT.Spaces.No.Negation.