proposition: Theorem evalZInv : forall v : rZ, evalZ (evalZ v) = evalZ v.
proof: Proof. intros v; case v; intros a; simpl in |- *; unfold evalN in |- *; CaseEq (rArrayGet _ Ar a); simpl in |- *; auto with stalmarck. intros r; case r; simpl in |- *; intros r0 H'; unfold evalN in |- *; CaseEq (rArrayGet _ Ar r0); auto with stalmarck; intros r1 H'1; Contradict H'1; apply wfPcr with (2 := H'); auto with stalmarck. intros l H'; unfold evalN in |- *; rewrite H'; auto with stalmarck. intros r; case r; simpl in |- *; intros r0 H'; unfold evalN in |- *; CaseEq (rArrayGet _ Ar r0); auto with stalmarck; intros r1 H'1; Contradict H'1; apply wfPcr with (2 := H'); auto with stalmarck. intros l H'; unfold evalN in |- *; rewrite H'; auto with stalmarck. Qed.