theorem NFA.valid_sorted_of_valid (captures : Array Capture) (h : Capture.Valid captures) : Capture.Valid (captures.mergeSort fun (a b : Capture) => decide (a ≤ b))

theorem NFA.valid_unique_of_valid (captures : Array Capture) (h : Capture.Valid captures) : Capture.Valid captures.unique

theorem NFA.CapturesValidOfRangeMap (captures : Array Capture) (h : List.map (fun (i : Nat) => if i % 2 = 0 then { role := Capture.Role.Start, group := i.div 2 } else { role := Capture.Role.End, group := i.div 2 }) (List.range captures.size) = captures.toList) : Capture.Valid captures