induction p using rec' generalizing n₂ μ₂ e <;>
  simp [Semiterm.subtEquiv_bind_eq_bind, bindq, Rew.rel, Rew.nrel, UFormula.bind,
    ofSubterm_eq_subtEquiv, ofSubformula_eq_subfEquiv, *]
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₂ : Type u_2
n₂ : ℕ
μ₁ : Type u_3
b : Fin n₁ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
p : Semiformula L μ₁ n₁
⊢ ↑(subfEquiv ((Rew.bind b e).hom p)) =
    UFormula.bind (fun x => if hx : x < n₁ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x)))
      ↑(subfEquiv p)
case hall
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (n✝ + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p✝)) =
      UFormula.bind (fun x => if hx : x < n✝ + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p✝)
μ₂ : Type u_2
n₂ : ℕ
b : Fin n✝ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ↑(subfEquiv ((Rew.bind b e).q.hom p✝)) =
    bindq (fun x => if hx : x < n✝ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x))) 1
      ↑(subfEquiv p✝)

case hex
L : Language
μ : Type v
α : Type u_1
inst✝⁵ : Primcodable α
inst✝⁴ : Primcodable μ
inst✝³ : (k : ℕ) → Primcodable (L.Func k)
inst✝² : UniformlyPrimcodable L.Func
inst✝¹ : (k : ℕ) → Primcodable (L.Rel k)
inst✝ : UniformlyPrimcodable L.Rel
n₁ : ℕ
μ₁ : Type u_3
n✝ : ℕ
p✝ : Semiformula L μ₁ (n✝ + 1)
a✝ :
  ∀ {μ₂ : Type u_2} {n₂ : ℕ} (b : Fin (n✝ + 1) → Semiterm L μ₂ n₂) (e : μ₁ → Semiterm L μ₂ n₂),
    ↑(subfEquiv ((Rew.bind b e).hom p✝)) =
      UFormula.bind (fun x => if hx : x < n✝ + 1 then ↑(subtEquiv (b ⟨x, hx⟩)) else default)
        (fun x => ↑(subtEquiv (e x))) ↑(subfEquiv p✝)
μ₂ : Type u_2
n₂ : ℕ
b : Fin n✝ → Semiterm L μ₂ n₂
e : μ₁ → Semiterm L μ₂ n₂
⊢ ↑(subfEquiv ((Rew.bind b e).q.hom p✝)) =
    bindq (fun x => if hx : x < n✝ then ↑(subtEquiv (b ⟨x, hx⟩)) else default) (fun x => ↑(subtEquiv (e x))) 1
      ↑(subfEquiv p✝)