proposition: Theorem rTreeDef1P : forall (t : rTreeP) (m : rNat) (v : Prop), rTreeGetP (rTreeSetP t m v) m = PSome 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: Coq(ZArith) Stalmarck(normalize) Coq(Classical) Stalmarck(sTactic)