proposition: Lemma parse_item'_ext (str : String) (str_matches_nonterminal str_matches_nonterminal' : nonterminal_carrierT -> parse_nt_T) (ext : forall s, str_matches_nonterminal s = str_matches_nonterminal' s) (offset : nat) (len : nat) (it : item Char) : parse_item' str str_matches_nonterminal offset len it = parse_item' str str_matches_nonterminal' offset len it.
proof: Proof. change ((pointwise_relation _ eq) str_matches_nonterminal str_matches_nonterminal') in ext. rewrite ext; reflexivity. Qed.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericRecognizer Fiat.Common Fiat.Common.Equality Fiat.Common.List.ListMorphisms