proposition: Theorem rArrayDef2P : forall (Ar : rArrayP) (m1 m2 : rNat) (v : Prop), m1 <> m2 -> rArrayGetP (rArraySetP Ar m1 v) m2 = rArrayGetP 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: Coq(ZArith) Stalmarck(normalize) Coq(Classical) Stalmarck(sTactic)