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. refine (parse_item_proj _ _ _ _ _ _ _); assumption. Qed.
imports: Fiat.Parsers.GenericRecognizerEquality Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BooleanRecognizer