proposition: Theorem wellFormedArrayInImpNotEq : forall (a b : rNat) (La Lb : list rZ), get Ar a = class La -> get Ar b = class Lb -> ~ InRz (rZPlus a) Lb.
proof: Proof. intros a b La Lb geta getb; red in |- *; intros H'3. case (InEqInv (rZPlus a) Lb H'3); intros H'4; auto with stalmarck. absurd (get Ar (valRz (rZPlus a)) = class La); auto with stalmarck. rewrite wfPcc1 with (1 := getb); auto with stalmarck. red in |- *; intro; discriminate. absurd (get Ar (valRz (rZMinus a)) = class La); auto with stalmarck. rewrite wfPcc1 with (1 := getb); auto with stalmarck. red in |- *; intro; discriminate. Qed.