simp[Semiformula.Operator.operator, Matrix.fun_eq_vec₂, operator_mem_def, memRelOpr]
ξ : Type u_1
n : ℕ
μ : Type u_2
Γ : Polarity
s : ℕ
t₁ t₂ u : Semiterm ℒₒᵣ μ n
⊢ Hierarchy Γ s (memRelOpr.operator ![u, t₁, t₂])
no goals