proposition: Lemma rdp_list_remove_nonterminal_noninc (ls : rdp_list_nonterminals_listT) nonterminal : ~ rdp_list_nonterminals_listT_R ls (rdp_list_remove_nonterminal ls nonterminal).
proof: Proof. simpl. unfold ltof, rdp_list_remove_nonterminal. fix_eqs. intro H. cut (Datatypes.length ls < Datatypes.length ls); try omega. eapply Nat.lt_le_trans; [ eassumption | ]. apply filter_list_dec. Qed.
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