theorem Regex.Data.Expr.empty_of_captures_of_nullOnly {s : String} {p p' : s.ValidPos} {groups : CaptureGroups s} {e : Expr} (c : Captures p p' groups e) (h : e.nullOnly = true) : p' = p

theorem Regex.Data.Expr.contains_get_of_captures_of_firstChars_some {s : String} {p p' : s.ValidPos} {groups : CaptureGroups s} {e : Expr} {n : ℕ} {cs : Std.HashSet Char} {ne : p ≠ s.endValidPos} (c : Captures p p' groups e) (h : firstChars n e = some cs) : cs.contains (p.get ne) = true