title: Omitting forall in Coq
body: <p>I found the <a href="http://lampwww.epfl.ch/~cremet/misc/confluence_ks/with_proofs/combinators.html" rel="nofollow">source code</a> of an interesting logical theorem that I want to work through. But when I run it in CoqIDE, it gets stuck near the very beginning.</p>
  
  <pre><code>Inductive Term: Set :=
     K: Term |
     S: Term |
     app: Term -&gt; Term -&gt; Term. 
  
  Inductive one_step: Term -&gt; Term -&gt; 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') -&gt; (one_step (app m n) (app m' n)) |
     redr: (m, n, n': Term) (one_step n n') -&gt; (one_step (app m n) (app m n')). 
  </code></pre>
  
  <p>Definition of <code>one_step</code> fails because <code>The reference m was not found in the current environment.</code></p>
  
  <p>I understand that the missing term is <code>forall</code>, but how did that original code run without it? Is there some module I need to load to make it implicit? </p>
  
  <p>A list of additional modules required to compile the code would also help very much, if there are any.</p>