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