Let r be given.

Assume Hr: r ∈ R.

We will prove apply_fun Romega_singleton_map r = Romega_singleton_seq r.

We prove the intermediate claim Hdef: Romega_singleton_map = graph R Romega_singleton_seq.

Use reflexivity.

rewrite the current goal using Hdef (from left to right).

An exact proof term for the current goal is (apply_fun_graph R Romega_singleton_seq r Hr).

∎