proposition: Theorem getRzMinEq2 : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (S : State), rArrayState Ar2 S -> forall a : rZ, eqStateRz S a (getRzMin Ar1 Ar2 a).
proof: Proof. intros Ar1 Ar2 War1 War2 S H' a; case a; intros a'; generalize (getEquivMinEq2 Ar1 Ar2 War1 War2 S H' a'); simpl in |- *; auto with stalmarck. Qed.