proposition: Lemma new_sigma2_sigma2_but_x_y : forall (s0 s1 : Site) (Data : Set) (f : Site -> Site -> Data -> Z) (t : Site -> Site -> Data), only_once Site eq_site_dec s0 LS1 -> only_once Site eq_site_dec s1 LS2 -> sigma2_table Site LS1 LS2 Data f t = (new_sigma2_but_table Site eq_site_dec LS1 LS2 Data s0 s1 f t + f s0 s1 (t s0 s1))%Z.
proof: Proof. intros s0 s1 Data0 f0 t H H0. unfold new_sigma2_but_table in |- *. rewrite sigma2_sigma2_but_x_y with (s0 := s0) (s1 := s1) (eq_site_dec := eq_site_dec). apply add_reduce17. rewrite sigma2_sigma2_but_x_y with (s0 := s0) (s1 := s1) (eq_site_dec := eq_site_dec). apply add_reduce18. apply sigma2_but_simpl. intros x y H1. case (eq_site_dec x s0); intro. case (eq_site_dec y s1); intro. elim H1; auto. auto. auto. auto. auto. rewrite case_eq. rewrite case_eq. auto. auto. auto. auto. auto. Qed.
imports: List fifo table reduce