proposition: Theorem wfPcc2 : forall (r : rNat) (s : rZ) (Ls : list rZ), get Ar r = ref s -> get Ar (valRz s) = class Ls -> In (samePol s r) Ls.
proof: Proof. intros r s Ls H' H'0; inversion War. inversion pC; apply H1 with (1 := H') (2 := H'0); auto with stalmarck. Qed.