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