simp [Rew.func, bv_func, Finset.biUnion_biUnion, *]
case func
L : Language
ξ : Type u_1
n k : ℕ
o : Operator L k
v : Fin k → Semiterm L ξ (n + 1)
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L Empty k
a_ih✝ : ∀ (a : Fin arity✝), ((Rew.substs v) (Rew.emb (a✝ a))).bv = (a✝ a).bv.biUnion fun i => (v i).bv
⊢ ((Rew.substs v) (Rew.emb (func a✝¹ a✝))).bv = (func a✝¹ a✝).bv.biUnion fun i => (v i).bv
no goals