{L : Type} {xL : L -> No} : forall (l:L) (r:Empty), xL l < Empty_rec r := fun l => Empty_ind _.
Require Import HoTT.Basics HoTT.Types. Require Import TruncType HSet. Require Import HoTT.Truncations.Core.