proposition: Remark del_trans_xi : forall s0 : Site, xi (delete_trans c0 s1) s0 = xi c0 s0.
proof: Proof. intro; unfold xi in |- *. rewrite del_trans_ctrl_copy. rewrite del_trans_rt. rewrite del_trans_ctrl_dec; rewrite case_eq. simpl in |- *; case (eq_site_dec s0 s1); intro. omega. trivial. trivial. Qed.
imports: init table_act mess_act