Let f be given.
Assume Hf: f ∈ image_of Romega_singleton_map R.
We will prove f ∈ Romega_tilde 0.
Apply (ReplE_impred R (λr0 : set ⇒ apply_fun Romega_singleton_map r0) f Hf (f ∈ Romega_tilde 0)) to the current goal.
Let r be given.
Assume Hr: r ∈ R.
Assume Hfeq: f = apply_fun Romega_singleton_map r.
rewrite the current goal using Hfeq (from left to right).
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_tilde0 r Hr).
∎