fact: Fixpoint rArraySetList (Ar : rArray vM) (a : rZ) (L : list rZ) {struct L} : rArray vM := match L with | nil => Ar | m :: ml' => rArraySet _ (rArraySetList Ar a ml') (valRz m) (ref (samePolRz m a)) end.