coq - 帰納型Coqからデータを取得する方法

Question

私は Coq に少し慣れていないので、Coq 内の通常の文法を形式化しようとしています。次のような誘導型があるとします。

Inductive rules : non_terminal -> list(non_terminal + terminal) -> Type :=
  rule1 : rules S [inr a; inl S] 
| rule2 : rules S [inr b;inl S] 
| rule3 : rules S [].

(a* b*)文法の派生規則を表します。後で使用するためにそれらを抽出したいとしましょう。これを実行してリストのリストに保存する方法はありますか? たとえば、私は私を返す手続きが欲しい[[S [inr a; inl S];S [inr b;inl S];[]]. 他のアイデアをいただければ幸いです。

前もって感謝します。