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. unfold parse_nonterminal_or_abort. revert valid offset len pf nt. match goal with | [ |- context[Fix ?wf _ _ ?a] ] => induction (wf a); intros end. rewrite !Fix5_eq by (intros; apply parse_nonterminal_step_ext; trivial). apply parse_nonterminal_step_proj; trivial. Qed.
imports: Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.GenericRecognizerExt Fiat.Common.Wf1 Fiat.Common.SetoidInstances Fiat.Parsers.GenericRecognizer