proposition: Lemma copy_trans_sigma_xi : sigma_xi (copy_trans c0 s1 s2) = (if eq_site_dec owner s1 then (sigma_xi c0 + 1)%Z else sigma_xi c0).
proof: Proof. unfold sigma_xi in |- *. case (eq_site_dec owner s1); intro. apply sigma__S with (eq_E_dec := eq_site_dec) (x0 := s2). exact finite_site. rewrite copy_trans_xi. rewrite e; rewrite case_eq; apply case_eq. intros; rewrite copy_trans_xi. rewrite e; rewrite case_eq; apply case_ineq; trivial. apply sigma_simpl; intros. rewrite copy_trans_xi; apply case_ineq; trivial. Qed.
imports: init table_act mess_act