proposition: Lemma pull_match_item {A R R' rn rc} {ls : item A} (f : R -> R') : match ls with | NonTerminal x => f (rn x) | Terminal x => f (rc x) end = f (match ls with | NonTerminal x => rn x | Terminal x => rc x end).
proof: Proof. destruct ls; reflexivity. Qed.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.StringLike.FirstCharSuchThat Coq.Strings.String Coq.Arith.PeanoNat Fiat.Computation.Core Coq.Program.Program Fiat.Computation.ApplyMonad Fiat.Computation.SetoidMorphisms Fiat.Common Fiat.Parsers.StringLike.Core Fiat.Parsers.ContextFreeGrammar.Equality Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common.Equality Fiat.Common.BoolFacts Fiat.Common.NatFacts Coq.Lists.List