exact absurd assm₁ (Nat.not_lt_of_le assm₂)
case base
nfa : NFA
next : Fin nfa.nodes.size
r : Expr
result : { nfa' // nfa.nodes.size < nfa'.nodes.size }
i' i : ℕ
cs : List Char
start : ℕ
eq : nfa.pushRegex next r = result
i✝ : ℕ
h✝ : start ≤ i✝
assm₁ : i✝ < nfa.nodes.size
assm₂ : nfa.nodes.size ≤ i✝
⊢ ∃ cs₁ cs₂,
    [] = cs₁ ++ cs₂ ∧ (↑result).pathToNext (↑next) nfa.nodes.size i✝ cs₁ ∧ (↑result).pathIn start (↑next) i✝ cs₂
no goals