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✝⁴
x✝¹ : Function.Injective x✝³
x✝ : Function.Injective x✝²
p : Semiformula L ξ✝ x✝⁶
⊢ (map x✝³ x✝²).hom ⊥ = (map x✝³ x✝²).hom p → ⊥ = p
no goals