proposition: Lemma rdp_list_ntl_wf : well_founded rdp_list_nonterminals_listT_R.
proof: Proof. unfold rdp_list_nonterminals_listT_R. intro. apply well_founded_ltof. Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common Fiat.Common.Equality Fiat.Common.List.Operations Fiat.Common.List.ListFacts