We will prove countable_set ω.

We will prove countable ω.

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

∎