proposition: Lemma ComputationalSplitter' : FullySharpened (string_spec paren_expr_grammar string_stringlike).
proof: Proof. splitter_start; splitter_finish. Defined.
imports: Fiat.Parsers.Refinement.Tactics Fiat.Parsers.Grammars.ExpressionParen