rintro rfl
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✝
t s : M
⊢ t = seqMap hf s →
    (Seq s →
        Seq t ∧ (∃ l ≤ 2 * s, l = lh s ∧ l = lh t) ∧ ∀ i < s, ∀ x < s, ⟪i, x⟫ ∈ s → ∃ y < t, y = f x ∧ ⟪i, y⟫ ∈ t) ∧
      (¬Seq s → t = 0)
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)