title: Can I use a notation for an Inductive type to define that type in Coq?
body: <p>Suppose I've got something like this:</p>
  
  <pre><code>Inductive SubtypeOf :
    Gamma -&gt; UnsafeType -&gt; Type -&gt; Set :=
  | SubRefl :
      forall (gamma : GammaEnv)  (u : UnsafeType)
      , SubtypeOf gamma u u
  | SubTrans :
      forall (gamma : GammaEnv)  (u1 u2 u3 : Type)
      , SubtypeOf gamma u1 u2
        -&gt; SubtypeOf gamma u2 u3
        -&gt; SubtypeOf gamma u1 u3.
  </code></pre>
  
  <p>And a notation defined:</p>
  
  <p><code>Notation "G |-  x &lt;: y " := (SubtypeOf G x y) (at level 50).</code></p>
  
  <p>Is there any way I can bring this notation into scope for the definition of <code>SubtypeOf</code>, so I could do something like this:</p>
  
  <pre><code>Inductive SubtypeOf :
    Gamma -&gt; UnsafeType -&gt; Type -&gt; Set :=
  | SubRefl :
      forall (gamma : GammaEnv)  (u : UnsafeType)
      ,  gamma |- u &lt;: u
  | SubTrans :
      forall (gamma : GammaEnv)  (u1 u2 u3 : Type)
      , gamma |- u1 &lt;: u2
        -&gt; gamma |- u2 &lt;: u3
        -&gt; gamma |- u1 &lt;: u3.
  </code></pre>