proposition: Lemma rcop3_trans_sigma_xi : sigma_xi (rec_copy3_trans c0 s1 s2) = (sigma_xi c0 + 1)%Z.
proof: Proof. unfold sigma_xi in |- *; apply sigma__S with (eq_E_dec := eq_site_dec) (x0 := s2). exact finite_site. rewrite (rcop3_trans_xi s2); apply case_eq. intros; rewrite rcop3_trans_xi; apply case_ineq; trivial. Qed.
imports: init table_act mess_act