by_cases hk : k' = 2 <;> simp [hk]
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₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
⊢ (k' = 2 ∧ HEq r' Language.Eq.eq ∧ HEq (fun i => ω (v i)) fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ k' = 2 ∧ HEq r' Language.Eq.eq ∧ HEq 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₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
hk : k' = 2
⊢ (HEq r' Language.Eq.eq ∧ HEq (fun i => ω (v i)) fun i => ![t, u] i) ↔
    ∃ t', ω t' = t ∧ ∃ x, ω x = u ∧ HEq r' Language.Eq.eq ∧ HEq v fun i => ![t', x] i