proposition: Theorem wellFormedArrayNInImpNotRef : forall (a : rNat) (b : rZ) (L : list rZ), get Ar a = class L -> ~ In b L -> get Ar (valRz b) <> ref (samePol b a).
proof: Proof. intros a b L H' H'0; Contradict H'0. cut (b = samePol (samePol b a) (valRz b)). intros H'1; rewrite H'1. apply (wfPcc2 (valRz b) (samePol b a) L); auto with stalmarck. rewrite <- H'; unfold get in |- *; auto with stalmarck. case b; simpl in |- *; auto with stalmarck. case b; simpl in |- *; auto with stalmarck. Qed.