proposition: Theorem updateEvalN2 : forall c d : rNat, evalN Ar c = evalN Ar d -> evalN (updateArray a b pol La Lb Ar) c = evalN (updateArray a b pol La Lb Ar) d.
proof: Proof. intros c d; case (rNatDec (valRz (evalN Ar c)) b); intros Eqt. rewrite updateEvalNb; auto with stalmarck. case (rNatDec (valRz (evalN Ar d)) b); intros Eqt'. rewrite updateEvalNb; auto with stalmarck. intros H'; rewrite H'; auto with stalmarck. intros H'; Contradict Eqt'; rewrite <- H'; auto with stalmarck. rewrite updateEvalNO; auto with stalmarck. case (rNatDec (valRz (evalN Ar d)) b); intros Eqt'. intros H'; Contradict Eqt; rewrite H'; auto with stalmarck. rewrite updateEvalNO; auto with stalmarck. Qed.