proposition: Lemma parse_item_proj str_matches_nonterminal str_matches_nonterminal' (H : forall nt, str_matches_nonterminal nt = str_matches_nonterminal' nt) (offset len : nat) (it : item _) : @parse_item' _ HSLM_lite _ _ (proj str) str_matches_nonterminal offset len it = @parse_item' _ HSLM_heavy _ _ str str_matches_nonterminal' offset len it.
proof: Proof. unfold parse_item'. destruct it; rewrite ?H; f_equal; try reflexivity. rewrite char_at_matches_proj, unsafe_get_proj; reflexivity. Qed.
imports: Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.GenericRecognizerExt Fiat.Common.Wf1 Fiat.Common.SetoidInstances Fiat.Parsers.GenericRecognizer