An exact proof term for the current goal is (Subq_atleastp Empty ω (Subq_Empty ω)).