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