by_cases hr : r' = r <;> simp[hr, Function.funext_iff]
case pos
L : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ : Type u_1
ξ₁ : Type u_2
ξ₂ : Type u_3
ξ₃ : Type u_4
n n₁ n₂✝ n₂ m m₁ m₂ m₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
k' : ℕ
r' : L.Rel k'
v✝ : Fin k' → Semiterm L ξ₁ n₁
r : L.Rel k'
v : Fin k' → Semiterm L ξ₂ n₂
⊢ r' = r ∧ (fun i => ω (v✝ i)) = v ↔ ⇑ω ∘ v✝ = v ∧ r' = r
no goals