Опуская forall в Coq

Question

Я нашел source code интересной логической теоремы, над которой хочу работать. Но когда я запускаю его в CoqIDE, он застревает в самом начале.

Inductive Term: Set := 
    K: Term | 
    S: Term | 
    app: Term -> Term -> Term. 

Inductive one_step: Term -> Term -> Prop := 
    redk: (m, n: Term) (one_step (app (app K m) n) m) | 
    reds: (m, n, p: Term) (one_step (app (app (app S m) n) p) (app (app m p) (app n p))) | 
    redl: (m, m', n: Term) (one_step m m') -> (one_step (app m n) (app m' n)) | 
    redr: (m, n, n': Term) (one_step n n') -> (one_step (app m n) (app m n')). 

Определение one_step терпит неудачу, потому что The reference m was not found in the current environment.

Я понимаю, что недостающий термин forall, но как это сделал оригинальный код запуска без него? Есть ли какой-то модуль, который мне нужно загрузить, чтобы сделать его неявным?

Список дополнительных модулей, необходимых для компиляции кода, также очень поможет, если таковые имеются.

Answer 1

Синтаксис немного изменился с версии 7.4, той, которая была протестирована с этой разработкой. Вот версия, которая работает на 8.4:

Inductive Term: Set := 
    K: Term | 
    S: Term | 
    app: Term -> Term -> Term. 

Inductive one_step: Term -> Term -> Prop := 
| redk (m n: Term) : one_step (app (app K m) n) m 
| reds (m n p: Term) : one_step (app (app (app S m) n) p) (app (app m p) (app n p)) 
| redl (m m' n: Term) : one_step m m' -> one_step (app m n) (app m' n) 
| redr (m n n': Term) : one_step n n' -> one_step (app m n) (app m n').