proposition: Theorem rArrayDef1 : forall (Ar : rArray) (m : rNat) (v : A), rArrayGet (rArraySet Ar m v) m = v.
proof: Proof. intros Ar m v; case Ar; simpl in |- *. intros r a; rewrite (rTreeDef1 r m v); auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)