proposition: Lemma fold_right_ret_orb_production_eq {Char} {gendata : @generic_parser_dataT Char} {gddata : generic_parser_decidable_data} {gdcdata : generic_parser_decidable_correctness_data} ls b : parse_production_T_to_bool (List.fold_right ret_orb_production b ls) = List.fold_right orb (parse_production_T_to_bool b) (List.map parse_production_T_to_bool ls).
proof: Proof. revert b; induction ls as [|?? IHls]; simpl; trivial; intros; []. rewrite <- IHls; clear IHls. autorewrite with generic_parser_decidable_correctness; trivial. Qed.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.GenericBaseTypes Fiat.Parsers.BaseTypes