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