Я пытаюсь доказать теорему о регулярных языках в CoqIDE.
Мне нужно разобрать гипотезу H1 : s1 \in "a" || "b" в H2 : s1 \in "a" без , создавая дополнительные подцели.
Я использовал inversion H2 tacti c, но это создало дополнительную подцель. Итак, возможно ли деконструировать гипотезу, не создавая дополнительных подцелей?
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"]