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

theorem Regex.Data.Expr.curr_of_captures_of_firstChars_some {it it' : String.Iterator} {groups : CaptureGroups} {e : Expr} {n : ℕ} {cs : Std.HashSet Char} (c : Captures it it' groups e) (h : firstChars n e = some cs) : cs.contains it.curr = true