proposition: Theorem updateArrayb : rArrayGet _ updateArray b = ref (samePolRz pol (rZPlus a)).
proof: Proof. unfold updateArray in |- *. cut (a <> b); [ intros Neqab | apply rltDef2; auto with stalmarck ]. rewrite rArrayDef2; auto with stalmarck. pattern b at 2 in |- *; replace b with (valRz (rZPlus b)); auto with stalmarck. rewrite rArraySetListInv2; auto with stalmarck. red in |- *; unfold appendRz in |- *; apply appendfOlist; auto with stalmarck. exact rZltEqComp. apply OlistOne; auto with stalmarck. apply wfOl with (2 := getb); auto with stalmarck. generalize appendfIncl1; unfold incl in |- *; auto with datatypes stalmarck. intros H'; unfold appendRz in |- *; apply H'; auto with datatypes stalmarck. apply DisjbLb with (2 := getb); auto with stalmarck. Qed.