proposition: Theorem rArrayStateEqState : forall (Ar : rArray vM) (S S' : State), rArrayState Ar S -> eqState S S' -> rArrayState Ar S'.
proof: Proof. intros Ar S S' H' H'0; red in |- *; split. intros H'1. apply rArrayStateDef1 with (S := S); auto with stalmarck. apply eqStateEq with (S1 := S'); auto with stalmarck. intros H'1. apply eqStateEq with (S1 := S); auto with stalmarck. apply rArrayStateDef2 with (Ar := Ar); auto with stalmarck. Qed.
imports: Stalmarck(stateDec)