proposition: Lemma new_string_of_base_string_R {str} : AbsR (projT2 splitter_impl) str (new_string_of_base_string str).
proof: Proof. unfold new_string_of_base_string. pose proof (ADTRefinementPreservesConstructors (projT2 splitter_impl) newS str (cConstructors (projT1 splitter_impl) newS str) (ReturnComputes _)) as H''; computes_to_inv; simpl in H''; computes_to_inv; subst; assumption. Qed.
imports: Coq.Strings.String Fiat.Common.BoundedLookup Fiat.ADT.ComputationalADT Fiat.ADTRefinement.GeneralRefinements Fiat.ADTRefinement.Core Fiat.ADTNotation.BuildADTSig Fiat.Parsers.GenericRecognizerEquality Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ParserADTSpecification Fiat.Parsers.ContextFreeGrammar.Valid Fiat.Parsers.ContextFreeGrammar.ValidReflective Fiat.Parsers.ParserImplementationOptimized Fiat.Parsers.ParserInterfaceReflective Fiat.Parsers.SplitterFromParserADT Fiat.Parsers.BaseTypes