proposition: Lemma pull_match_list {A R R' rn rc} {ls : list A} (f : R -> R') : match ls with | nil => f rn | cons x xs => f (rc x xs) end = f (match ls with | nil => rn | cons x xs => rc x xs 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