no goals
α : Type u
β : Type v
γ : Type w
s : WSeq α
m n : ℕ
h : m ≤ n
⊢ Terminates (get? s n) → Terminates (get? s m)
induction' h with m' _ IH <;> [exact id;
  exact fun T => IH (@head_terminates_of_head_tail_terminates _ _ T)]