proposition: Theorem rArrayDef : forall (m : rNat) (f : rNat -> A), rArrayGet (rArrayInit f) m = f m.
proof: Proof. intros m f; simpl in |- *; auto with stalmarck. elim m; simpl in |- *; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)