The add-one-variable recurrence for hSub

hSub (insert j A) (m+1) = hSub A (m+1) + X j * hSub (insert j A) m

theorem RS.hSub_insert {k : ℕ} {A : Finset (Fin k)} {j : Fin k} (hj : j ∉ A) (m : ℕ) : hSub (insert j A) (m + 1) = hSub A (m + 1) + MvPolynomial.X j * hSub (insert j A) m

The add-one-variable recurrence: terms either avoid the new variable or use it at least once.