proposition: Theorem rArrayDefP : forall (m : rNat) (f : rNat -> Prop), rArrayGetP (rArrayInitP f) m = f m.
proof: Proof. intros m f; simpl in |- *; auto with stalmarck. elim m; simpl in |- *; auto with stalmarck. Qed.
imports: Coq(ZArith) Stalmarck(normalize) Coq(Classical) Stalmarck(sTactic)