proposition: Theorem rTreeDef2 : forall (t : rTree) (m1 m2 : rNat) (v : A), m1 <> m2 -> rTreeGet (rTreeSet t m1 v) m2 = rTreeGet t m2.
proof: Proof. intros t m; generalize t; Elimc m; simpl in |- *; clear t. intros p H' t m2 v; case m2; simpl in |- *; case t; auto with stalmarck. intros p0 H'0; rewrite H'; auto with stalmarck. elim p0; simpl in |- *; auto with stalmarck. Contradict H'0; rewrite H'0; auto with stalmarck. intros a r1 r2 p0 H'0; rewrite H'; auto with stalmarck. Contradict H'0; rewrite H'0; auto with stalmarck. intros p0 H'0; elim p0; simpl in |- *; auto with stalmarck. intros p H' t m2 v; case m2; simpl in |- *; case t; auto with stalmarck. intros p0 H'0; elim p0; simpl in |- *; auto with stalmarck. intros p0 H'0; rewrite H'; auto with stalmarck. elim p0; simpl in |- *; auto with stalmarck. Contradict H'0; rewrite H'0; auto with stalmarck. intros a r1 r2 p0 H'0; rewrite H'; auto with stalmarck. Contradict H'0; rewrite H'0; auto with stalmarck. intros t m2 v; case m2; simpl in |- *; auto with stalmarck. case t; intros p H'; elim p; simpl in |- *; auto with stalmarck. case t; intros p H'; elim p; simpl in |- *; auto with stalmarck. intros H'; Contradict H'; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)