proposition: Theorem updateWellFormed : wellFormedArray updateArray.
proof: Proof. apply wellFormedArrayDef; auto with stalmarck. apply updateArrayPointerDecrease; auto with stalmarck. apply updateArrayPointToRef; auto with stalmarck. apply updateArrayPointToClassClass; auto with stalmarck. apply updateArrayOlist; auto with stalmarck. Qed.