theorem Regex.Syntax.Parser.Ast.toRegexAux_tags {index index' : ℕ} {ast : Ast} {e : Data.Expr} (h : toRegexAux index ast = (index', e)) : index ≤ index' ∧ e.tags = Finset.Ico index index'

theorem Regex.Syntax.Parser.Ast.toRegexAux_disjoint (index : ℕ) (ast : Ast) : (toRegexAux index ast).2.Disjoint

theorem Regex.Syntax.Parser.Ast.toRegex_disjoint (ast : Ast) : ast.toRegex.Disjoint

theorem Regex.Syntax.Parser.Ast.toRegexAux_group_of_group {ast : Ast} : (toRegexAux 0 ast.group).2 = Data.Expr.group 0 (toRegexAux 1 ast).2

theorem Regex.Syntax.Parser.Ast.toRegex_group_of_group (ast : Ast) : ∃ (e : Data.Expr), ast.group.toRegex = Data.Expr.group 0 e