proposition: Theorem rArrayStateGet : forall (Ar Ar' : rArray vM) (S : State), rArrayState Ar S -> (forall e : rNat, rArrayGet vM Ar' e = rArrayGet vM Ar e) -> rArrayState Ar' S.
proof: Proof. intros Ar Ar' S H' H'0. red in |- *; split; repeat rewrite <- (rArrayGetEvalZ _ _ H'0); auto with stalmarck; case (H' c d); auto with stalmarck. Qed.
imports: Stalmarck(stateDec)