proposition: Theorem wellFormedArrayInRzBothImpEq : forall (a b : rNat) (c : rZ) (La Lb : list rZ), get Ar a = class La -> get Ar b = class Lb -> InRz c La -> InRz c Lb -> a = b.
proof: Proof. intros a b c La Lb H'0 H'1 H'2 H'3. case (InEqInv c La H'2); case (InEqInv c Lb H'3); intros H'4 H'5; apply wellFormedArrayInBothImpEq with (1 := H'0) (2 := H'1) (3 := H'5) (4 := H'4); auto with stalmarck. Qed.