proposition: Theorem eqStateRarray : forall (Ar Ar' : rArray vM) (S S' : State), rArrayState Ar S -> rArrayState Ar' S' -> (forall e : rNat, rArrayGet vM Ar' e = rArrayGet vM Ar e) -> eqState S S'.
proof: Proof. intros Ar Ar' S S' H' H'0 H'1; red in |- *; split. red in |- *; intros i j H; case (H'0 i j); intros H1 H2; apply H2. repeat rewrite <- (rArrayGetEvalZ Ar Ar'); auto with stalmarck. case (H' i j); auto with stalmarck. red in |- *; intros i j H; case (H' i j); intros H1 H2; apply H2. repeat rewrite <- (rArrayGetEvalZ Ar' Ar); auto with stalmarck. case (H'0 i j); auto with stalmarck. Qed.