proposition: Lemma item_rvalid_correct {it} : is_true (item_rvalid it) <-> item_valid it.
proof: Proof. destruct it; simpl; unfold is_true; try tauto. Qed.
imports: Coq.Strings.String Coq.Lists.List Coq.Arith.PeanoNat Fiat.Parsers.StringLike.Core Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Valid