Let n be given.

Assume HnO: n ∈ ω.

Apply set_ext to the current goal.

An exact proof term for the current goal is (Romega_tilde_subspace_box_subspace_product n HnO).

An exact proof term for the current goal is (Romega_tilde_subspace_product_subspace_box n HnO).

∎