We will prove apply_fun double_map_left_half (eps_ 1) = 1.

rewrite the current goal using (double_map_apply (eps_ 1) eps_1_in_unit_interval_left_half) (from left to right).

An exact proof term for the current goal is eps_1_half_eq2.

∎