proposition: Lemma ComputationalSplitter : FullySharpened (string_spec ab_star_grammar HSL).
proof: Proof. make_simplified_splitter ComputationalSplitter'. Defined.
imports: Fiat.Parsers.Grammars.ABStar Fiat.Parsers.Refinement.Tactics