proposition: Theorem WarCompEq : forall Ar1 Ar2 : rArray vM, (forall a : rNat, get Ar1 a = get Ar2 a) -> wellFormedArray Ar1 -> wellFormedArray Ar2.
proof: Proof. intros Ar1 Ar2 H' War1; inversion War1. apply wellFormedArrayDef; auto with stalmarck. apply pointerDecreaseDef; auto with stalmarck. intros r s; rewrite <- H'; inversion pD; auto with stalmarck. apply pointToClassRefDef; auto with stalmarck. intros r s t; repeat rewrite <- H'; auto with stalmarck. intros H'0; inversion pR; auto with stalmarck. apply H0 with (r := r); auto with stalmarck. apply pointToClassClassRef; auto with stalmarck. intros r s Lr; repeat rewrite <- H'; auto with stalmarck. intros H'0 H'1; inversion pC; auto with stalmarck. apply H0 with (Lr := Lr); auto with stalmarck. intros r s Ls; repeat rewrite <- H'; auto with stalmarck. intros H'0 H'1; inversion pC; auto with stalmarck. apply OlistArrayDef; auto with stalmarck. intros r Lr; repeat rewrite <- H'; auto with stalmarck. intros H'0; inversion oC; auto with stalmarck. apply H0 with (r := r); auto with stalmarck. Qed.