proposition: Theorem rArrayDef2 : forall (Ar : rArray) (m1 m2 : rNat) (v : A), m1 <> m2 -> rArrayGet (rArraySet Ar m1 v) m2 = rArrayGet Ar m2.
proof: Proof. intros Ar m1 m2 v H'; case Ar; simpl in |- *. intros r a; rewrite (rTreeDef2 r m1 m2 v); auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)