proposition: Theorem rTreeDef1 : forall (t : rTree) (m : rNat) (v : A), rTreeGet (rTreeSet t m v) m = Some v.
proof: Proof. intros t m; generalize t; Elimc m; simpl in |- *; clear t. intros p H' t v; case t; auto with stalmarck. intros p H' t v; case t; auto with stalmarck. intros t v; case t; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)