誘導型の表記法を使用してCoqでその型を定義できますか？

Question

私はこのような何か持っていると仮定します。

Inductive SubtypeOf : 
    Gamma -> UnsafeType -> Type -> Set := 
| SubRefl : 
    forall (gamma : GammaEnv) (u : UnsafeType) 
    , SubtypeOf gamma u u 
| SubTrans : 
    forall (gamma : GammaEnv) (u1 u2 u3 : Type) 
    , SubtypeOf gamma u1 u2 
     -> SubtypeOf gamma u2 u3 
     -> SubtypeOf gamma u1 u3. 

と定義された表記：

Notation "G |- x <: y " := (SubtypeOf G x y) (at level 50).

は私が、SubtypeOfの定義については、スコープにこの表記をもたらすことができる方法はあります私はこのような何かができる：

Inductive SubtypeOf : 
    Gamma -> UnsafeType -> Type -> Set := 
| SubRefl : 
    forall (gamma : GammaEnv) (u : UnsafeType) 
    , gamma |- u <: u 
| SubTrans : 
    forall (gamma : GammaEnv) (u1 u2 u3 : Type) 
    , gamma |- u1 <: u2 
     -> gamma |- u2 <: u3 
     -> gamma |- u1 <: u3. 

Answer 1

ejgallegoさんのコメントを拡張し、ドキュメントがありますReserved Notationsおよびa where clause for inductivesのための記法。 <:はむしろxに吸収されるよりも、|-で解析されますように、私たちは、次のレベル（49）でxを置く必要があります

Reserved Notation "G |- x <: y" (at level 50, x at next level). 
Definition UnsafeType := Type. 
Axiom Gamma : Set. 
Notation GammaEnv := Gamma. 
Inductive SubtypeOf : 
    Gamma -> UnsafeType -> Type -> Type := 
| SubRefl : 
    forall (gamma : GammaEnv) (u : UnsafeType) 
    , gamma |- u <: u 
| SubTrans : 
    forall (gamma : GammaEnv) (u1 u2 u3 : Type) 
    , gamma |- u1 <: u2 
     -> gamma |- u2 <: u3 
     -> gamma |- u1 <: u3 
where "G |- x <: y " := (SubtypeOf G x y). 

注：ここでは動作するコードです。