Remove unnecessarily restrictive type signature
Replace obsolete static lemma numbers with labels
Make Horner's rule for arrays a lemma