proposition: Lemma might_be_empty_parse_of (nt : String.string) (str : String) (Hlen : length str = 0) (p : parse_of G str (Lookup G nt)) : collapse_might_be_empty (might_be_empty_nt G nt) = true.
proof: Proof. unfold might_be_empty_nt. rewrite fgd_fold_grammar_correct. apply (fold_grammar_correct eq_refl) in p. destruct p as [P [Hp0 p]]. lazymatch goal with | [ p : related _ (lookup_state ?st ?nt) |- collapse_might_be_empty (lookup_state ?st ?nt') = true ] => change nt' with nt; destruct (lookup_state) as [|[]|] eqn:H end; [ reflexivity | | | ]; simpl in p; unfold might_be_empty_accurate in p; try specialize (p eq_refl); try specialize (p _ Hp0); (congruence || tauto). Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.StringLike.Properties Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Fix.FromAbstractInterpretationDefinitions Fiat.Parsers.ContextFreeGrammar.Fix.Fix Fiat.Parsers.ContextFreeGrammar.Fix.FromAbstractInterpretation Fiat.Common