An exact proof term for the current goal is (apply_fun_graph R (λy0 : set ⇒ (div_SNo c a,y0)) y HyR).