no goals
α : Type u
β : Type v
γ : Type w
s : Seq α
⊢ ¬Terminates s ↔ ∀ (n : ℕ), Option.isSome (get? s n) = true
simp only [Terminates, TerminatedAt, ← Ne.def, Option.ne_none_iff_isSome, not_exists, iff_self]