proposition: Theorem initCorrect : rArrayState (rArrayInit _ (fun n : rNat => class nil)) nil.
proof: Proof. red in |- *; intros c d; split; intros H'. cut (eqConstrState nil c d). intros H'0; inversion H'0; auto with stalmarck. apply eqStateRzPImpeqConstrState; auto with stalmarck. generalize H'; case c; case d; simpl in |- *; unfold evalN in |- *; intros r r0; rewrite (rArrayDef vM r0 (fun _ : rNat => class nil)); rewrite (rArrayDef vM r (fun _ : rNat => class nil)); simpl in |- *; intros H'0; rewrite H'0 || rewrite <- H'0; auto with stalmarck. Qed.
imports: Stalmarck(stateDec)