我正在尝试证明CoqIDE中的常规语言定理。
我需要将假设H1 : s1 \in "a" || "b"分解为H2 : s1 \in "a"，无需创建其他子目标。
我使用了inversion H2策略，但它创建了其他子目标。因此，有可能在不创建其他子目标的情况下解构假设吗？
3 subgoals
w : word
H : w \in ("a" || "b");; "c"
s1,s2,s3 : list ascii
H1 : s1 \in "a" || "b"
______________________________________(1/3)
w = ["a"; "c"]