proposition: Lemma parse_production_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 (prod : @production_carrierT _ data) : @parse_production' _ HSLM_lite _ _ (proj str) len0 parse_nonterminal offset len0_minus_len prod = @parse_production' _ HSLM_heavy _ _ str len0 parse_nonterminal' offset len0_minus_len prod.
proof: Proof. unfold parse_production', parse_production'_for. simpl. set (ls := @to_production Char predata prod). generalize (eq_refl : to_production prod = ls). clearbody ls. revert prod offset len0_minus_len; induction ls; simpl; intros ??? Heq. { reflexivity. } { f_equal; []. rewrite split_string_for_production_proj. apply map_Proper_eq; trivial; []. intro. rewrite IHls. { f_equal; []. rewrite ?Heq. apply parse_item_proj; trivial. } { simpl; rewrite production_tl_correct, Heq; reflexivity. } } Qed.
imports: Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.GenericRecognizerExt Fiat.Common.Wf1 Fiat.Common.SetoidInstances Fiat.Parsers.GenericRecognizer