proposition: Theorem rArrayGetEvalN : forall Ar Ar' : rArray vM, (forall e : rNat, rArrayGet vM Ar' e = rArrayGet vM Ar e) -> forall e : rNat, evalN Ar e = evalN Ar' e.
proof: Proof. intros Ar Ar' H' e; unfold evalN in |- *. rewrite (H' e); auto with stalmarck. Qed.