theorem Regex.NFA.pushRegex_size_lt {nfa : NFA} {next : Nat} {e : Data.Expr} : nfa.size < (nfa.pushRegex next e).size

theorem Regex.NFA.pushRegex_wf {nfa : NFA} {next : Nat} {e : Data.Expr} (wf : nfa.WellFormed) (next_lt : next < nfa.size) : (nfa.pushRegex next e).WellFormed

theorem Regex.NFA.compile_wf {e : Data.Expr} : (compile e).WellFormed

theorem Regex.NFA.pushRegex_get_lt {nfa : NFA} {next : Nat} {e : Data.Expr} (i : Nat) (h : i < nfa.size) : (nfa.pushRegex next e)[i] = nfa[i]