theorem Regex.NFA.Compile.ProofData.Group.castFromExpr [Group] {it it' : String.Iterator} {update : List (ℕ × String.Pos)} (path : nfaExpr.Path nfaClose.nodes.size nfaExpr.start it nfaClose.start it' update) : nfa'.Path nfaClose.nodes.size nfaExpr.start it nfaClose.start it' update

theorem Regex.NFA.Compile.ProofData.Group.castToExpr [Group] {it it' : String.Iterator} {update : List (ℕ × String.Pos)} {lb j : ℕ} (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) (path : nfa'.Path lb nfaExpr.start it j it' update) : nfaExpr.Path lb nfaExpr.start it j it' update

theorem Regex.NFA.Compile.ProofData.Alternate.castFrom₁ [Alternate] {it it' : String.Iterator} {update : List (ℕ × String.Pos)} (path : nfa₁.Path nfa.nodes.size nfa₁.start it next it' update) : nfa'.Path nfa.nodes.size nfa₁.start it next it' update

theorem Regex.NFA.Compile.ProofData.Alternate.castFrom₂ [Alternate] {it it' : String.Iterator} {update : List (ℕ × String.Pos)} (path : nfa₂.Path nfa.nodes.size nfa₂.start it next it' update) : nfa'.Path nfa.nodes.size nfa₂.start it next it' update

theorem Regex.NFA.Compile.ProofData.Alternate.castTo₁ [Alternate] {it it' : String.Iterator} {update : List (ℕ × String.Pos)} (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) (path : nfa'.Path nfa.nodes.size nfa₁.start it next it' update) : nfa₁.Path nfa.nodes.size nfa₁.start it next it' update

theorem Regex.NFA.Compile.ProofData.Alternate.castTo₂ [Alternate] {it it' : String.Iterator} {update : List (ℕ × String.Pos)} {lb : ℕ} (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) (path : nfa'.Path lb nfa₂.start it next it' update) : nfa₂.Path lb nfa₂.start it next it' update

theorem Regex.NFA.Compile.ProofData.Concat.castFrom₂ [Concat] {it it' : String.Iterator} {update : List (ℕ × String.Pos)} (path : nfa₂.Path nfa.nodes.size nfa₂.start it next it' update) : nfa'.Path nfa.nodes.size nfa₂.start it next it' update

theorem Regex.NFA.Compile.ProofData.Concat.castTo₂ [Concat] {it it' : String.Iterator} {update : List (ℕ × String.Pos)} (wf : nfa.WellFormed) (next_lt : next < nfa.nodes.size) (path : nfa'.Path nfa.nodes.size nfa₂.start it next it' update) : nfa₂.Path nfa.nodes.size nfa₂.start it next it' update

theorem Regex.NFA.Compile.ProofData.Star.castFromExpr [Star] {it it' : String.Iterator} {update : List (ℕ × String.Pos)} (path : nfaExpr.Path nfaPlaceholder.nodes.size nfaExpr.start it nfaPlaceholder.start it' update) : nfa'.Path nfaPlaceholder.nodes.size nfaExpr.start it nfaPlaceholder.start it' update

theorem Regex.NFA.Compile.ProofData.Star.castToExpr [Star] {it it' : String.Iterator} {update : List (ℕ × String.Pos)} (wf : nfa.WellFormed) (path : nfa'.Path nfaPlaceholder.nodes.size nfaExpr.start it nfaPlaceholder.start it' update) : nfaExpr.Path nfaPlaceholder.nodes.size nfaExpr.start it nfaPlaceholder.start it' update