We will prove function_on Romega_singleton_map R R_omega_space.
Let r be given.
Assume Hr: r ∈ R.
We will prove apply_fun Romega_singleton_map r ∈ R_omega_space.
rewrite the current goal using (Romega_singleton_map_apply r Hr) (from left to right).
An exact proof term for the current goal is (Romega_singleton_seq_in_Romega_space r Hr).
∎