proposition: Theorem GetClassNProp : forall (Ar : rArray vM) (a : rZ), wellFormedArray Ar -> rArrayGet vM Ar (valRz (evalZ Ar a)) = class (getClassN Ar (valRz (evalZ Ar a))).
proof: Proof. intros Ar a War; case a; simpl in |- *; unfold evalN, getClassN in |- *; intros r; generalize (fun s => wfPcr _ War r s); CaseEq (rArrayGet vM Ar r); simpl in |- *. intros r0 H' H'0; CaseEq (rArrayGet vM Ar (valRz r0)); auto with stalmarck. intros r1 H'1; case (H'0 r0 r1); auto with stalmarck. intros l H'; rewrite H'; auto with stalmarck. intros r0 H' H'0; rewrite (valRzComp r0); CaseEq (rArrayGet vM Ar (valRz r0)); auto with stalmarck. intros r1 H'1; case (H'0 r0 r1); auto with stalmarck. intros l H'; rewrite H'; auto with stalmarck. Qed.