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. unfold parse_nonterminal_step. unfold sumbool_rect; simpl. repeat match goal with | [ |- context[match ?e with _ => _ end] ] => destruct e eqn:? | _ => solve [ erewrite parse_productions_proj; try reflexivity; cbv beta; trivial ] | _ => reflexivity | _ => progress simpl @option_rect end. Qed.
imports: Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.GenericRecognizerExt Fiat.Common.Wf1 Fiat.Common.SetoidInstances Fiat.Parsers.GenericRecognizer