proposition: Lemma item_valid_proof_irrelevance {it : item Char} (x y : item_valid it) : x = y.
proof: Proof. destruct it; simpl in *; try destruct x, y; trivial. apply dec_eq_uip; decide equality. 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