proposition: Lemma rt_root : rt c0 (root_parent s0) = true.
proof: Proof. unfold root_parent in |- *; apply prop_root. trivial. intros; apply parent_rt with (s0 := y); trivial. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc