proposition: Theorem updateArrayInb : forall c : rZ, In c Lb -> rArrayGet _ updateArray (valRz c) = ref (samePolRz c (samePolRz pol (rZPlus a))).
proof: Proof. intros c InLb; unfold updateArray in |- *. rewrite rArrayDef2; 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 appendfIncl2; unfold incl in |- *; auto with datatypes stalmarck. unfold appendRz in |- *; intros H'; apply H'; auto with stalmarck. apply DisjbLb with (2 := getb); auto with stalmarck. red in |- *; intros H'; absurd (InRz (rZPlus a) Lb); auto with stalmarck. apply wellFormedArrayInImpNotEq with (2 := geta) (3 := getb); auto with stalmarck. rewrite H'; auto with stalmarck. red in |- *; apply InEqComp with (a := c); auto with stalmarck. apply inImpInEq; auto with stalmarck. Qed.