cases p using cases' <;> simp[Rew.rel, Rew.nrel]
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
p : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom (nrel r v) = (map x✝¹ x✝).hom p → nrel r v = p
case hnrel
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₃ x✝⁴ x✝³ : ℕ
ξ✝ : Type u_5
x✝² : Type u_6
x✝¹ : Fin x✝⁴ → Fin x✝³
x✝ : ξ✝ → x✝²
hb : Function.Injective x✝¹
hf : Function.Injective x✝
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ξ✝ x✝⁴
k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L ξ✝ x✝⁴
⊢ arity✝ = k✝ →
    HEq r r✝ → (HEq (fun i => (map x✝¹ x✝) (v i)) fun i => (map x✝¹ x✝) (v✝ i)) → arity✝ = k✝ ∧ HEq r r✝ ∧ HEq v v✝