proposition: Theorem updateGetIsClass : forall (r : rNat) (Lr : list rZ), rArrayGet _ updateArray r = class Lr -> r <> a -> rArrayGet _ Ar r = class Lr.
proof: Proof. intros r Lr H' H'0. case (rNatDec r b); intros Eqb; auto with stalmarck. generalize H'; rewrite Eqb; auto with stalmarck; rewrite updateArrayb; clear H'; intros H'; discriminate. case (InRzDec (rZPlus r) Lb); intros InRLb; auto with stalmarck. case (InEqInv (rZPlus r) Lb); auto with stalmarck; intros InRLb'. generalize H'; replace r with (valRz (rZPlus r)); auto with stalmarck; rewrite updateArrayInb; auto with stalmarck; clear H'; intros H'; discriminate. generalize H'; replace r with (valRz (rZMinus r)); auto with stalmarck; rewrite updateArrayInb; auto with stalmarck; clear H'; intros H'; discriminate. rewrite <- H'; apply sym_equal. apply updateArrayOtherwise; auto with stalmarck. Qed.