proposition: Lemma sub_nonterminals_listT_remove_3 {ls ls' p} (H0 : is_valid_nonterminal ls p = false) (H1 : sub_nonterminals_listT ls ls') : sub_nonterminals_listT ls (remove_nonterminal ls' p).
proof: Proof. intros p' H'. rewrite remove_nonterminal_5; intuition (subst; eauto; congruence). Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.RelationClasses Coq.Setoids.Setoid Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes