apply @seq_induction M _ _ _ _ _ _ 𝚺
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
⊢ Seq s → ∃ t, Seq t ∧ lh t = lh s ∧ ∀ i < lh s, ∀ x < s, ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t
case hP
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
⊢ (𝚺, 1)-Predicate fun {s} => ∃ t, Seq t ∧ lh t = lh s ∧ ∀ i < lh s, ∀ x < s, ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t

case hnil
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
⊢ ∃ t, Seq t ∧ lh t = lh ∅ ∧ ∀ i < lh ∅, ∀ x < ∅, ⟪i, x⟫ ∈ ∅ → ⟪i, f x⟫ ∈ t

case hcons
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
⊢ ∀ (s x : M),
    Seq s →
      (∃ t, Seq t ∧ lh t = lh s ∧ ∀ i < lh s, ∀ x < s, ⟪i, x⟫ ∈ s → ⟪i, f x⟫ ∈ t) →
        ∃ t, Seq t ∧ lh t = lh (s ⁀' x) ∧ ∀ i < lh (s ⁀' x), ∀ x_1 < s ⁀' x, ⟪i, x_1⟫ ∈ s ⁀' x → ⟪i, f x_1⟫ ∈ t