Как поставить 'a является подмножеством b'in coq?

Question

Я пытался реализовать, что S - это подмножество Z, используя Infix "⊂": = (Включено Z) (на уровне 70).(наш проф предоставил это, но когда я пытаюсь написать forall (S ⊂ Z), (вставьте теорему) появляется сообщение об ошибке, как показано ниже

Синтаксическая ошибка: ',' ожидается после [constr: open_binders] (в [constr: binder_constr]).

Есть предложения?

Answer 1

В квантификаторе могут отображаться только переменные.Вам нужно поместить формулу в гипотезу внутри квантификатора, например:

forall S, S ⊂ Z -> (* Some property *)