proposition: Theorem rArraySetListInv1 : forall (Ar : rArray vM) (a : rZ) (mL : list rZ) (m : rZ), ~ InRz m mL -> rArrayGet _ (rArraySetList Ar a mL) (valRz m) = rArrayGet _ Ar (valRz m).
proof: Proof. intros Ar a mL; generalize Ar; Elimc mL; clear Ar; simpl in |- *; auto with stalmarck. intros a0 l H' Ar m H'0. rewrite rArrayDef2; auto with stalmarck. apply H'; auto with stalmarck. Contradict H'0; auto with stalmarck. red in |- *; apply InEqSkip; auto with stalmarck. Contradict H'0; auto with stalmarck. red in |- *; apply InEqHead; auto with stalmarck; red in |- *; auto with stalmarck. Qed.