rewrite the current goal using (apply_fun_graph unit_interval_right_half (λt0 : set ⇒ add_SNo (mul_SNo 2 t0) (minus_SNo 1)) t Ht) (from left to right).