proposition: Lemma parse_nonterminal_step_proj (len0 valid_len : nat) parse_nonterminal parse_nonterminal' (H : forall p pf valid offset len pf' nt, parse_nonterminal p pf valid offset len pf' nt = parse_nonterminal' p pf valid offset len pf' nt) valid offset len pf nt : @parse_nonterminal_step _ HSLM_lite _ (proj str) len0 valid_len parse_nonterminal valid offset len pf nt = @parse_nonterminal_step _ HSLM_heavy _ str len0 valid_len parse_nonterminal' valid offset len pf nt.
proof: Proof. refine (parse_nonterminal_step_proj _ _ _ _ _ _ _ _); assumption. Qed.
imports: Fiat.Parsers.GenericRecognizerEquality Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BooleanRecognizer