proposition: Theorem getNotIdP : forall r : rZ, get Ar (valRz r) <> ref r.
proof: Proof. intros r; red in |- *; intros H'. absurd (rVlt r (valRz r)); auto with stalmarck. unfold rVlt in |- *; auto with stalmarck. apply wfPd; auto with stalmarck. Qed.