proposition: Theorem evalZTrue : evalZ rZTrue = rZTrue.
proof: Proof. simpl in |- *; unfold evalN in |- *. generalize (fun s : rZ => wfPd _ War zero s); case (rArrayGet vM Ar zero); auto with stalmarck. intros r H'; absurd (rVlt r zero); auto with stalmarck. Qed.