proposition: Lemma grammar_rvalid_correct : is_true grammar_rvalid <-> grammar_valid G.
proof: Proof. unfold grammar_rvalid, grammar_valid. induction (Valid_nonterminals G); t ltac:(idtac; match goal with | [ |- productions_valid _ ] => apply productions_rvalid_correct | [ H : context[productions_valid _] |- _ ] => setoid_rewrite <- productions_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