(P : No -> Type) `{forall x, IsHProp (P x)} (dcut : forall (L R : Type) (s : InSort S L R) (xL : L -> No) (xR : R -> No) (xcut : forall (l:L) (r:R), (xL l) < (xR r)) (IHL : forall l, P (xL l)) (IHR : forall r, P (xR r)), P {{ xL | xR // xcut }}) (x : No) : P x. Proof. revert x; refine (No_ind P (fun _ _ _ _ _ => Unit) (fun _ _ _ _ _ => Unit) _ _ _ _ _); intros; try apply path_ishprop; try exact tt. apply dcut; assumption. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.