by_cases H : Seq s <;> simp only [H, Seq.seqMap, lt_succ_iff_le, Seq.seqMap_lh_eq, and_self,
  exists_eq_right, lh_bound, true_and, forall_true_left, not_true_eq_false, IsEmpty.forall_iff, and_true,
  not_false_eq_true, H, seqMap_spec_of_not_seq, forall_true_left]
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H : Seq s✝
s : M
⊢ (Seq s →
      Seq (seqMap hf s) ∧
        (∃ l ≤ 2 * s, l = lh s ∧ l = lh (seqMap hf s)) ∧
          ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < seqMap hf s, y = f x ∧ ⟪i, y⟫ ∈ seqMap hf s) ∧
    (¬Seq s → seqMap hf s = 0)
case pos
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚺₁
f : M → M
hf : 𝚺₁-Function₁ f
s✝ : M
H✝ : Seq s✝
s : M
H : Seq s
⊢ ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < seqMap hf s, y = f x ∧ ⟪i, y⟫ ∈ seqMap hf s