proposition: Theorem updateArraya : rArrayGet _ updateArray a = class (fappendRz La (appendRz (rZPlus b :: nil) Lb)).
proof: Proof. unfold updateArray in |- *; unfold LetP in |- *; simpl in |- *. rewrite rArrayDef1; auto with stalmarck. Qed.