proposition: Lemma productions_valid_app (pat pat' : productions Char) (H : productions_valid (pat ++ pat')) : productions_valid pat'.
proof: Proof. induction pat; simpl in *; trivial. eapply IHpat, productions_valid_cons; eassumption. Qed.
imports: Coq.Strings.String Coq.Lists.List Fiat.Parsers.StringLike.Core Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Equality Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Valid Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Common Fiat.Common.UIP Fiat.Common.List.ListFacts