proposition: Lemma production_valid_cons (it : item Char) (its : production Char) (H : production_valid (it :: its)) : production_valid its.
proof: Proof. unfold production_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