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