theorem MvPolynomial.rename_killCompl_app {τ : Type u_1} {σ : Type u_2} {R : Type u_3} [CommSemiring R] {f : σ → τ} (hf : Function.Injective f) {p : MvPolynomial τ R} (hp : ↑p.vars ⊆ Set.range f) : (rename f) ((killCompl hf) p) = p