proposition: Lemma ComputationalSplitter' : FullySharpened (string_spec plus_expr_grammar string_stringlike).
proof: Proof. start sharpening ADT. start honing parser using indexed representation. hone method "splits". { Time simplify parser splitter. { Time refine_disjoint_search_for. } simpl. finish honing parser method. } finish_Sharpening_SplitterADT. Defined.
imports: Fiat.Parsers.Refinement.Tactics Fiat.Parsers.Grammars.ExpressionNumPlus Fiat.Parsers.Refinement.DisjointRules Fiat.Parsers.ExtrOcamlParsers