proposition: Theorem rArraySetListInv2 : forall (Ar : rArray vM) (a : rZ) (mL : list rZ) (m : rZ), OlistRz mL -> In m mL -> rArrayGet _ (rArraySetList Ar a mL) (valRz m) = ref (samePolRz m a).
proof: Proof. intros Ar a mL; generalize Ar; elim mL; simpl in |- *; auto with stalmarck. intros Ar0 m H' H'0; elim H'0; auto with stalmarck. intros a0 l H' Ar0 m H'0 H'1; Elimc H'1; intros H'1; [ rewrite <- H'1 | idtac ]; auto with stalmarck. apply rArrayDef1; auto with stalmarck. rewrite rArrayDef2; auto with stalmarck. apply H'; auto with stalmarck. red in |- *; apply OlistInv with (a := a0); auto with stalmarck. red in |- *; intros H'2; absurd (InEq _ eqRz m l); auto with stalmarck. apply OlistUniqueEq with (ltA := rZlt) (a := a0); auto with stalmarck. exact rZltEqComp. apply inImpInEq; auto with stalmarck. Qed.