proposition: Theorem refSameEq : forall (a b : rZ) (r s : rNat), ref (samePol a s) = ref (samePol b r) -> s = r.
proof: Proof. intros a b r s; case a; case b; simpl in |- *; intros a1 b1 C1; inversion C1; auto with stalmarck. Qed.