(x y : GenNo) (p : x <= y) : dle x y p (No_ind x) (No_ind y) := match No_Empty_admitted with end.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.