proposition: Lemma productions_valid_cons (p : production Char) (ps : productions Char) (H : productions_valid (p :: ps)) : productions_valid ps.
proof: Proof. unfold productions_valid in *. inversion H; subst; assumption. 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