proposition: Theorem updateArrayPointToRef : pointToClassRef updateArray.
proof: Proof. apply pointToClassRefDef; auto with stalmarck. intros r s t H'1. case (rNatDec (valRz s) a); intros eqsa. rewrite eqsa; auto with stalmarck; rewrite updateArraya; red in |- *; intros H'2; discriminate. case (rNatDec r a); intros eqra. generalize H'1; rewrite eqra; auto with stalmarck; rewrite updateArraya; auto with stalmarck; intros; discriminate. case (rNatDec r b); intros eqrb; auto with stalmarck. generalize H'1; rewrite eqrb; auto with stalmarck; rewrite updateArrayb; auto with stalmarck; clear H'1; intros H'1; case eqsa; inversion H'1. apply samePolRzValRz; auto with stalmarck. case (InRzDec (rZPlus r) Lb); intros InRLb; auto with stalmarck. case (InEqInv (rZPlus r) Lb); auto with stalmarck; intros InRLb'. generalize H'1; replace r with (valRz (rZPlus r)); auto with stalmarck; rewrite updateArrayInb; auto with stalmarck; clear H'1; intros H'1; case eqsa; inversion H'1; simpl in |- *; auto with stalmarck. apply samePolRzValRz; auto with stalmarck. generalize H'1; replace r with (valRz (rZMinus r)); auto with stalmarck; rewrite updateArrayInb; auto with stalmarck; clear H'1; intros H'1; case eqsa; inversion H'1; simpl in |- *; auto with stalmarck. simpl in |- *; rewrite valRzComp; rewrite samePolRzValRz; auto with stalmarck. generalize H'1; auto with stalmarck; rewrite updateArrayOtherwise; auto with stalmarck; clear H'1; intros H'1. case (rNatDec (valRz s) b); intros eqsb; auto with stalmarck. case InRLb; red in |- *. apply InEqComp with (a := samePol s r); auto with stalmarck. apply inImpInEq; auto with stalmarck. apply wfPcc2 with (Ar := Ar); auto with stalmarck. rewrite eqsb; auto with stalmarck; rewrite updateArrayb; auto with stalmarck. case s; simpl in |- *; auto with stalmarck. case (InRzDec s Lb); intros InRLb'; auto with stalmarck. case (InEqInv s Lb); auto with stalmarck; intros InRLb''. absurd (rArrayGet _ Ar (valRz s) = ref (samePol s b)); auto with stalmarck. inversion War. inversion pR. apply H0 with (r := r); auto with stalmarck. inversion War. inversion pC. apply H0 with (Lr := Lb); auto with stalmarck. absurd (rArrayGet _ Ar (valRz (rZComp s)) = ref (samePol (rZComp s) b)). rewrite valRzComp; auto with stalmarck. inversion War. inversion pR. apply H0 with (r := r); auto with stalmarck. inversion War. inversion pC. apply H0 with (Lr := Lb); auto with stalmarck. rewrite updateArrayOtherwise; auto with stalmarck. inversion War. inversion pR. apply H0 with (r := r); auto with stalmarck. red in |- *; intros H'2; case InRLb'; red in |- *. apply InEqComp with (a := rZPlus (valRz s)); auto with stalmarck. Qed.