proposition: Lemma productions_valid_proof_irrelevance {p : productions Char} (x y : productions_valid p) : x = y.
proof: Proof. apply Forall_proof_irrelevance, @production_valid_proof_irrelevance. 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