proposition: Lemma parse_productions_proj (len0 : nat) parse_nonterminal parse_nonterminal' (H : forall offset len0_minus_len nt, parse_nonterminal offset len0_minus_len nt = parse_nonterminal' offset len0_minus_len nt) offset len0_minus_len prods : @parse_productions' _ HSLM_lite _ _ (proj str) len0 parse_nonterminal offset len0_minus_len prods = @parse_productions' _ HSLM_heavy _ _ str len0 parse_nonterminal' offset len0_minus_len prods.
proof: Proof. unfold parse_productions'. f_equal; []. apply map_Proper_eq; trivial; []. intro. apply parse_production_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