case rel => rcases eq with ⟨v', rfl, rfl⟩; simp
L : Language
inst✝ : L.LT
μ : Type v
μ₁ : Type u_1
μ₂ : Type u_2
n₂ : ℕ
Γ : Polarity
s : ℕ
q : Semiformula L μ₂ n₂
x✝ : ℕ
Γ✝ : Polarity
s✝ k✝ : ℕ
r✝ : L.Rel k✝
v✝ : Fin k✝ → Semiterm L μ₂ x✝
n₁ : ℕ
ω : Rew L μ₁ n₁ μ₂ x✝
p : Semiformula L μ₁ n₁
eq : ∃ v', ⇑ω ∘ v' = v✝ ∧ p = Semiformula.rel r✝ v'
⊢ Hierarchy Γ✝ s✝ p
no goals