proposition: Remark no_ancestor_s2 : forall s : Site, ~ ancestor c0 s2 s.
proof: Proof. intro; red in |- *; intro; absurd (false = rt c0 s2). apply true_not_false; apply (ancestor_rt s); trivial. auto. Qed.
imports: init table_act mess_act