theorem Regex.find_str_eq_some {re : Regex} {haystack : String} {slice : String.Slice} (h : re.find haystack = some slice) : slice.str = haystack

theorem Regex.captures_of_find_some {re : Regex} {haystack : String} {slice : String.Slice} (h : re.find haystack = some slice) (isr : re.IsSearchRegex) : Matches.Spec isr haystack haystack.startPosPlusOne slice ⋯

theorem Regex.captures_of_mem_findAll {re : Regex} {haystack : String} {slice : String.Slice} (mem : slice ∈ re.findAll haystack) (isr : re.IsSearchRegex) : ∃ (startPos : haystack.PosPlusOne) (eq : slice.str = haystack), Matches.Spec isr haystack startPos slice eq

theorem Regex.captures_of_capture_some {re : Regex} {haystack : String} {captured : CapturedGroups haystack} (h : re.capture haystack = some captured) (isr : re.IsSearchRegex) : CapturedGroups.Spec isr haystack haystack.startPosPlusOne captured

theorem Regex.captures_of_mem_captureAll {re : Regex} {haystack : String} {captured : CapturedGroups haystack} (mem : captured ∈ re.captureAll haystack) (isr : re.IsSearchRegex) : ∃ (startPos : haystack.PosPlusOne), CapturedGroups.Spec isr haystack startPos captured