proposition: Lemma ancestor_rt : forall s1 s2 : Site, ancestor c0 s2 s1 -> rt c0 s2 = true.
proof: Proof. intros; elim H. intros; apply parent_rt with (s0 := s3); trivial. intros; apply parent_rt with (s0 := s3); trivial. Qed.
imports: copy del rece_copy1 rece_copy2 rece_copy3 rece_dec rece_inc