proposition: Theorem evalNEvalZ : forall Ar Ar' : rArray vM, (forall e : rNat, evalN Ar e = evalN Ar' e) -> forall e : rZ, evalZ Ar e = evalZ Ar' e.
proof: Proof. intros Ar Ar' H' e; case e; simpl in |- *; auto with stalmarck. intros r; rewrite H'; auto with stalmarck. Qed.