proposition: Theorem updateEvalZ2Comp : forall c d : rZ, evalZ Ar c = rZComp (evalZ Ar d) -> evalZ (updateArray a b pol La Lb Ar) c = rZComp (evalZ (updateArray a b pol La Lb Ar) d).
proof: Proof. intros c d; repeat rewrite <- evalZComp. intros H'; apply updateEvalZ2; auto with stalmarck. Qed.