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