cases r 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✝
p q r : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom (p ⋏ q) = (map x✝¹ x✝).hom r → p ⋏ q = r
case hand
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✝
p q p✝ q✝ : Semiformula L ξ✝ x✝⁴
⊢ (map x✝¹ x✝).hom p = (map x✝¹ x✝).hom p✝ → (map x✝¹ x✝).hom q = (map x✝¹ x✝).hom q✝ → p = p✝ ∧ q = q✝