title: Using tuples when constructing inductive types
body: <p>I'm trying to use a pair to pass as an argument into an inductive type in Coq</p>
  <pre><code>Definition pair := (nat,nat).
  
  Inductive use_pair :=
    | mktriplet : pair -&gt; nat -&gt; use_pair.
  </code></pre>
  <p>However, this gives the error:</p>
  <pre><code>Error: In environment
  use_pair : Type
  The term &quot;pair&quot; has type &quot;(Set * Set)%type&quot;
  which should be Set, Prop or Type.
  </code></pre>
  <p>I can get this to work</p>
  <pre><code>Inductive use_pair :=
    | mktriplet : (Set * Set) -&gt; nat -&gt; use_pair.
  </code></pre>
  <p>But I would like to specify that the <em>only</em> tuple which will work is <code>(nat,nat)</code>.</p>
  <p>How can I specify this? I see the notation scope <code>%type</code> but that seems different than <code>Type</code>, though I don't know how to experiment with this; <code>Check type</code> returns an error.</p>