proposition: Theorem wellFormedArrayInImpNotEqSimpl : forall (a : rNat) (La : list rZ), get Ar a = class La -> ~ InRz (rZPlus a) La.
proof: Proof. intros a La H'. apply wellFormedArrayInImpNotEq with (1 := H') (2 := H'); auto with stalmarck. Qed.