Coq证明泵引理提示存在未聚焦目标但无法聚焦剩余目标

我正在尝试证明泵引理（pumping Lemma），这是《Logical Foundations》教材中的一道习题。我本以为已经完成了MStarApp分支的证明，但Coq解释器提示仍存在未聚焦的剩余目标。我始终无法将该剩余目标切换为当前证明焦点，尝试了所有层级的bullet都返回错误提示[Focus] Wrong bullet: No more goals.，无法确定是自身证明逻辑存在错误还是解释器出现bug。

对应证明代码片段 #

- (* MStarApp *)
    intros.
    destruct s1.
    -- replace ([ ] ++ s2) with s2 in *. apply (IH2 H).
       reflexivity.
    -- pose proof (lt_ge_cases (length (x::s1)) (pumping_constant re)) as [
    Hs1lt | Hs1ge].
      --- exists [ ], (x::s1), s2. repeat split.
        + unfold not. intro. inversion H0.
        + simpl. simpl in Hs1lt. 
          apply n_lt_m__n_le_m in Hs1lt.
          apply Hs1lt.
        + simpl. intro m. 
          apply (napp_star T m (x::s1) s2 re Hmatch1 Hmatch2).
      --- unfold ge in Hs1ge. pose proof (IH1 Hs1ge) as [
        s2' [s3' [s4' [Hxs1Eq [Hs3notEmpty [
        Hlens2's3' Hnapp]]]]]].
        exists s2', s3', (s4' ++ s2). repeat split.
        + rewrite Hxs1Eq. repeat rewrite <- app_assoc.
          reflexivity.
        + assumption.
        + simpl. assumption.
        + intro m. pose proof Hnapp m.
          replace (s2' ++ napp m s3' ++ s4' ++ s2) with 
          ((s2' ++ napp m s3' ++ s4') ++ s2).
          constructor.
          ++ assumption.
          ++ assumption.
          ++ repeat rewrite <- app_assoc. reflexivity.
(* 此处Coq提示: 'There are unfocused goals.' *)

补充信息 #

不确定该信息是否与问题相关：在证明的上层（MApp分支）中，编写的assert语句闭合花括号高亮显示异常，使用VSCode的Coq语言支持扩展时，正常闭合括号应为绿色高亮，此处显示为黄色，异常效果如下：

内容的提问来源于stack exchange，提问作者user566206