proposition: Theorem forallgetEquivgetRzMin : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (S : State), (forall a : rNat, eqStateRz S (rZPlus a) (getEquivMin Ar1 Ar2 a)) -> forall a : rZ, eqStateRz S a (getRzMin Ar1 Ar2 a).
proof: Proof. intros Ar1 Ar2 War1 War2 S H' a; case a; intros a'; simpl in |- *; auto with stalmarck. apply eqStateRzInv with (1 := H' a'); auto with stalmarck. Qed.