title: How to extend a grammar in coq?
body: <pre><code>Inductive ty0: Type :=
  | Bool : ty0
  | Int : ty0
  | Dyn : ty0
  | Arrow0: ty0 -&gt; ty0 -&gt; ty0.
  
  Inductive ty1: Type := 
  | ty : ty0 -&gt; ty1
  | Inters : ty1 -&gt; ty1 -&gt; ty1.
  
  Inductive ty2: Type :=
  | ty': ty0 -&gt; ty2
  | Arrow2 : ty1 -&gt; ty2 -&gt; ty2.
  
  Inductive consist : ty2 -&gt; ty2 -&gt; Prop :=
   | cs_dyn1 : forall t2, consist Dyn t2
  </code></pre>
  
  <p>I have a grammar, which is ty0, and I want to create a grammar t1 which is t0 and other things. So far, I have no problem compiling this. But when I define "consist" and I say  <code>consist Dyn t2</code> it says that Dyn is actually t0 and it's expecting t2. How do I tell it that t2 is t0 plus other things?</p>
  
  <p>Edited relation:</p>
  
  <pre><code>Coercion ty0_ty2 (t : ty0) : ty2 := (ty' t).
  Coercion ty0_ty1 (t : ty0) : ty1 := (ty t).
  
  Inductive consist0 : ty0 -&gt; ty0 -&gt; Prop := 
  | cs_dyn1 : forall t2, consist0 Dyn t2
  | cs_dyn2 : forall t1, consist0 t1  Dyn
  | cs_same : forall t1, consist0 t1 t1
  | cs_arrow0 : forall t1 t2 t1' t2', consist0 t1 t1' -&gt; 
                                      consist0 t2 t2'-&gt;
   consist0 (Arrow0 t1 t2) (Arrow0 t1' t2').
  
  Inductive consist1 : ty1 -&gt; ty1 -&gt; Prop :=
  | cs_same1 : forall t1, consist1 t1 t1
  | cs_consist0 : forall t1 t2, consist0 t1 t2 -&gt; consist1 t1 t2
  | c_inters : forall t1 t2 t1' t2', consist1 t1 t1' -&gt; 
  consist1 t2 t2'-&gt;
  consist1 (Inters t1 t2) (Inters t1' t2').
  
  Inductive consist : ty2 -&gt; ty2 -&gt; Prop :=
    | cs_consist1 : forall t1 t2, consist0 t1 t2 -&gt; consist t1 t2
    | cs_arrow2 : forall t1 t2 t1' t2', consist1 t1 t1' -&gt; 
                                        consist t2 t2'-&gt;
     consist (Arrow2 t1 t2) (Arrow2 t1' t2').
  </code></pre>