proposition: Lemma parse_item'_eq str_matches_nonterminal str_matches_nonterminal' (str_matches_nonterminal_eq : forall nt, parse_nt_T_to_bool (gendata := gendata) (str_matches_nonterminal nt) = parse_nt_T_to_bool (gendata := gendata') (str_matches_nonterminal' nt)) (offset : nat) (len : nat) (it : item Char) : parse_item_T_to_bool (parse_item' (gendata := gendata) str str_matches_nonterminal offset len it) = parse_item_T_to_bool (parse_item' (gendata := gendata') str str_matches_nonterminal' offset len it).
proof: Proof. t I. Qed.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericBoolCorrectnessBaseTypes Fiat.Parsers.GenericRecognizer Fiat.Parsers.GenericRecognizerExt Fiat.Common Fiat.Common.Wf1