proposition: Theorem wellFormedArrayInImpLt : forall (a : rNat) (b : rZ) (La : list rZ), get Ar a = class La -> In b La -> rlt a (valRz b).
proof: Proof. intros a b La geta Inb. replace a with (valRz (samePol b a)). generalize (wfPd _ _ (wfPcc1 _ _ _ geta Inb)); unfold rVlt in |- *; auto with stalmarck. case b; case a; simpl in |- *; auto with stalmarck. Qed.