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_firstChar_some {it it' : String.Iterator} {groups : CaptureGroups} {e : Expr} {ch : Char} (c : Captures it it' groups e) (h : e.firstChar = some ch) : it.curr = ch