proposition: Theorem wellFormedArrayInBothImpEq : forall (a b : rNat) (c d : rZ) (La Lb : list rZ), get Ar a = class La -> get Ar b = class Lb -> In c La -> In d Lb -> eqRz c d -> a = b.
proof: Proof. intros a b c d La Lb geta getb inc1 inc2 eqRz1. apply refSameEq with (a := c) (b := d). rewrite <- wfPcc1 with (1 := geta); auto with stalmarck. rewrite <- wfPcc1 with (1 := getb); auto with stalmarck. rewrite eqRz1; auto with stalmarck. Qed.