(x y : GenNo S) : (No_raise x <= No_raise y) -> (x <= y) := fst (No_raise_reflects_lelt x y).
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.