proposition: Theorem updateEvalZ2 : forall c d : rZ, evalZ Ar c = evalZ Ar d -> evalZ (updateArray a b pol La Lb Ar) c = evalZ (updateArray a b pol La Lb Ar) d.
proof: Proof. intros c d; case c; case d; simpl in |- *; intros; try apply EqrZComp; try apply updateEvalN2 || apply updateEvalN2Comp; auto with stalmarck. apply sym_equal; apply updateEvalN2Comp; auto with stalmarck. generalize H; case (evalN Ar r0); case (evalN Ar r); simpl in |- *; intros r1 r2 H'; inversion H'; auto with stalmarck. Qed.