proposition: Theorem getEquivMinEq1 : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (S : State), rArrayState Ar1 S -> forall a : rNat, eqStateRz S (rZPlus a) (getEquivMin Ar1 Ar2 a).
proof: Proof. intros Ar1 Ar2 War1 War2 S H' a. apply rArrayStateDef2 with (Ar := Ar1); auto with stalmarck. case (getEquivListProp1 Ar1 War1 (rZPlus a) (getEquivMin Ar1 Ar2 a)). intros H'0; rewrite H'0; auto with stalmarck. apply getEquivMinIn1; auto with stalmarck. Qed.