Omega Pow seq prop

theorem omegaPow_seq_prop [Inhabited α] :    l^ω = { s : ωSequence α |      ∃ f : ℕ → ℕ, StrictMono f ∧ f 0 = 0 ∧ ∀ m, s.extract (f m) (f (m + 1)) ∈ l } := by  ext s; constructor  · rintro ⟨xs, rfl, h_xs⟩    simp [forall_and, List.ne_nil_iff_length_pos] at h_xs    refine ⟨xs.cumLen, by grind [cumLen_strictMono], by simp [cumLen_zero], ?_⟩    grind  · rintro ⟨f, hm, h0, he⟩    refine ⟨(fun m ↦ s.extract (f m) (f (m + 1))), ?_, ?_⟩    · apply strictMono_flatten hm h0    · intro m      change s.extract (f m) (f (m + 1)) ∈ l - 1      simp only [he, Language.mem_sub_one, ne_eq, extract_eq_nil_iff, ge_iff_le, not_le, true_and]      apply hm; omega