У меня есть функция содержит:
Fixpoint contains (l: list string) (x: string): bool :=
match l with
| [] => false
| h :: tl => (if (string_dec h x) then true else (contains tl x))
end.
, которая проверяет, есть ли строка в списке строк. Я хотел бы доказать теорему, выполнив анализ случая того, действительно ли contains (vars e) y Однако, когда я уничтожаю это логическое значение, я не получаю никакой дополнительной гипотезы для разных подслучаев.
Как я могу решить эту проблему?