Heap: parametrise all modules over, instead of postulate ∣Heap∣ : ℕ

∙ As suggested/demanded by @jmchapman