proposition: Lemma sigma2_table_simpl_property : forall (t : Site -> Site -> Data) (P : (Site -> Site -> Data) -> Site -> Site -> Set) (f1 f2 : Site -> Site -> Data -> Z), (forall (s1 s2 : Site) (d : Data), P t s1 s2 -> f1 s1 s2 d = f2 s1 s2 d) -> (forall s1 s2 : Site, P t s1 s2) -> sigma2_table Site LS1 LS2 Data f1 t = sigma2_table Site LS1 LS2 Data f2 t.
proof: Proof. intros t0 P f1' f2' H. unfold sigma2_table in |- *. intro H0. apply sigma_table_simpl_property with (P := fun (t : Site -> Z) (s2 : Site) => P t0 s1 s2). intros H1. apply funct_eq. intros e. apply sigma_table_simpl2. intros s d. apply H. auto. auto. Qed.
imports: List fifo table reduce