by_cases hr : r' = Language.Eq.eq <;> simp [hr, Function.funext_iff]
case pos
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
⊢ (r' = Language.Eq.eq ∧ (fun i => ω (v i)) = fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ r' = Language.Eq.eq ∧ v = fun i => ![t', x] i
case pos
L✝ : Language
L L' : Language
L₁ : Language
L₂ : Language
L₃ : Language
ξ ξ' : Type v
ξ₁ : Type v₁
ξ₂ : Type v₂
ξ₃ : Type v₃
n n₁ n₂ n₃ : ℕ
ω : Rew L ξ₁ n₁ ξ₂ n₂
inst✝ : L.Eq
t u : Semiterm L ξ₂ n₂
r' : L.Rel 2
v : Fin 2 → Semiterm L ξ₁ n₁
hr : r' = Language.Eq.eq
⊢ (∀ (a : Fin 2), ω (v a) = ![t, u] a) ↔ ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ ∀ (a : Fin 2), v a = ![t', x] a