by_cases hk : k' = k <;> simp[hk]
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₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
⊢ k' = k ∧ HEq r' r ∧ HEq (fun i => ω (v i)) v✝ ↔ ∃ v', ⇑ω ∘ v' = v✝ ∧ k' = k ∧ HEq r' r ∧ HEq v v'
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₂
k' : ℕ
r' : L.Rel k'
v : Fin k' → Semiterm L ξ₁ n₁
hk : k' = k
⊢ HEq r' r ∧ HEq (fun i => ω (v i)) v✝ ↔ ∃ v', ⇑ω ∘ v' = v✝ ∧ HEq r' r ∧ HEq v v'