proposition: Lemma FirstStep_helper_gen {P Q} (H : forall r_n offset len d x0, refine (expanded_fallback_list' P r_n offset len d x0) (expanded_fallback_list' Q r_n offset len d x0)) : refineADT (rindexed_spec' P) (rindexed_spec' Q).
proof: Proof. econstructor 1; try instantiate (1 := eq); eapply Iterate_Ensemble_BoundedIndex_equiv; try apply string_dec; simpl; intros; repeat split; try solve [ intuition; intros; try simplify with monad laws; repeat intro; computes_to_inv; subst; simpl; fin ]. intros; subst. setoid_rewrite refineEquiv_pick_eq'. simplify with monad laws. assert (H' : forall A B (x : A * B), (fst x, snd x) = x) by (intros; destruct x; reflexivity). setoid_rewrite H'. simplify with monad laws. apply H. Defined.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Arith.PeanoNat Coq.Lists.List Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ParserInterface Fiat.Parsers.ParserADTSpecification Fiat.Parsers.ContextFreeGrammar.Equality Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Parsers.Refinement.FixedLengthLemmas Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.ADT.ComputationalADT Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements.HoneRepresentation Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.Common Fiat.Common.Equality Fiat.Common.StringBound Fiat.Common.ilist Fiat.Common.IterateBoundedIndex Fiat.Common.List.FlattenList Fiat.Common.List.ListMorphisms Fiat.Common.List.ListFacts Fiat.Common.NatFacts Fiat.Common.StringFacts Fiat.Common.LogicFacts Fiat.Common.LogicMorphisms Fiat.Computation.SetoidMorphisms Fiat.Common.List.ListMorphisms Fiat.Common.Instances Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Common Fiat.Common.Enumerable Fiat.Common.Enumerable.BoolProp Fiat.Common.Enumerable.ReflectiveForall Fiat.Common.Enumerable.ReflectiveForallStaged