proposition: Lemma parse_nonterminal_or_abort_proj (p : nat * nat) (valid : nonterminals_listT) (offset len : nat) (pf : len <= fst p) nt : @parse_nonterminal_or_abort _ HSLM_lite _ (proj str) p valid offset len pf nt = @parse_nonterminal_or_abort _ HSLM_heavy _ str p valid offset len pf nt.
proof: Proof. refine (parse_nonterminal_or_abort_proj _ _ _ _ _ _); assumption. Qed.
imports: Fiat.Parsers.GenericRecognizerEquality Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BooleanRecognizer