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

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

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

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

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

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

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

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

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

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