proposition: Lemma production_rvalid_correct {pat} : is_true (production_rvalid pat) <-> production_valid pat.
proof: Proof. unfold production_rvalid, production_valid. induction pat; t ltac:(idtac; match goal with | [ |- item_valid _ ] => apply item_rvalid_correct | [ H : item_valid _ |- _ ] => apply item_rvalid_correct in H end). 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