case hall ih =>
  exact ih (fun x => by cases x using Fin.cases <;> simp[hb]) (fun x hx => by simp; exact congr_arg _ (hf x hx))
L : Language
ξ : Type u_1
n n₁ n₂✝ m m₁ m₂ m₃ : ℕ
ξ₁ : Type u_2
ξ₂ : Type u_3
n✝ : ℕ
p✝ : Semiformula L ξ₁ (n✝ + 1)
ih :
  ∀ {n₂ : ℕ} {ω₁ ω₂ : Rew L ξ₁ (n✝ + 1) ξ₂ n₂},
    (∀ (x : Fin (n✝ + 1)), ω₁ #x = ω₂ #x) →
      Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar) → ω₁.hom p✝ = ω₂.hom p✝
n₂ : ℕ
ω₁ ω₂ : Rew L ξ₁ n✝ ξ₂ n₂
hb : ∀ (x : Fin n✝), ω₁ #x = ω₂ #x
hf : Function.funEqOn (fun x => x ∈ p✝.fvarList) (⇑ω₁ ∘ Semiterm.fvar) (⇑ω₂ ∘ Semiterm.fvar)
⊢ ω₁.q.hom p✝ = ω₂.q.hom p✝
no goals