proposition: Lemma FirstStep_gen : refineADT (string_spec G HSL) opt_rindexed_spec_gen.
proof: Proof. apply (projT2 FirstStep_sig_gen). Qed.
imports: Coq.Strings.String Fiat.Common.List.ListFacts Fiat.ADTNotation.BuildADT Fiat.ADTNotation.BuildADTSig Fiat.ADT.ComputationalADT Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements.HoneRepresentation Fiat.Parsers.ParserADTSpecification Fiat.Parsers.Refinement.IndexedAndAtMostOneNonTerminalReflective Fiat.Parsers.StringLike.Core Fiat.Parsers.ContextFreeGrammar.Precompute Fiat.Parsers.BaseTypes Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.ContextFreeGrammar.PreNotations