proposition: Theorem rArrayStateDef2 : forall (Ar : rArray vM) (S : State) (c d : rZ), rArrayState Ar S -> evalZ Ar c = evalZ Ar d -> eqStateRz S c d.
proof: Proof. intros Ar S c d H' H'0; case (H' c d); auto with stalmarck. Qed.
imports: Stalmarck(stateDec)