proposition: Theorem rArrayGetEvalZ : forall Ar Ar' : rArray vM, (forall e : rNat, rArrayGet vM Ar' e = rArrayGet vM Ar e) -> forall e : rZ, evalZ Ar e = evalZ Ar' e.
proof: Proof. intros Ar Ar' H' e; apply evalNEvalZ; auto with stalmarck. intros e'; apply rArrayGetEvalN; auto with stalmarck. Qed.