proposition: Theorem getEquivIdL : forall (Ar1 Ar2 : rArray vM) (War1 : wellFormedArray Ar1) (War2 : wellFormedArray Ar2) (S1 S2 : State), rArrayState Ar1 S1 -> rArrayState Ar2 S2 -> forall a : rNat, eqStateRz S1 (rZPlus a) (evalZ Ar2 (rZPlus a)) -> getEquivMin Ar1 Ar2 a = evalZ Ar2 (rZPlus a).
proof: Proof. intros Ar1 Ar2 War1 War2 S1 S2 H' H'0 a H'1. rewrite getEquivMinSym; auto with stalmarck. apply getEquivIdR with (S1 := S2) (S2 := S1); auto with stalmarck. Qed.