proposition: Lemma parse_production'_helper {offset len0_minus_len it its} (pf : length (substring offset (len0 - len0_minus_len) str) <= len0) : dec {n0 : nat & (minimal_parse_of_item (G := G) len0 valid (take n0 (substring offset (len0 - len0_minus_len) str)) it * minimal_parse_of_production (G := G) len0 valid (drop n0 (substring offset (len0 - len0_minus_len) str)) its)%type} -> dec (minimal_parse_of_production (G := G) len0 valid (substring offset (len0 - len0_minus_len) str) (it :: its)).
proof: Proof. intros [H|H]; [ left; destruct H as [n [??]] | right; intro p; apply H; clear H ]. { econstructor; eassumption. } { clear -p; abstract (inversion p; subst; eexists; split; eassumption). } Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Arith.EqNat Coq.Arith.Compare_dec Coq.Arith.Wf_nat Coq.ZArith.ZArith Fiat.Common.List.Operations Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericCorrectnessBaseTypes Fiat.Parsers.StringLike.Properties Fiat.Parsers.MinimalParse Fiat.Parsers.CorrectnessBaseTypes Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.WellFoundedParse Fiat.Parsers.MinimalParseOfParse Fiat.Parsers.GenericRecognizer Fiat.Parsers.GenericRecognizerExt Fiat.Common.Wf Fiat.Common.Wf1 Fiat.Common.List.ListFacts Fiat.Common.NatFacts Fiat.Common.UIP Fiat.Common