proposition: Lemma xif_sum_zero: forall b i k (f: nat -> X A B), xif b (sum i k f) 0 == sum i k (fun j => xif b (f j) 0).
proof: Proof. intros. revert i. induction k; intro i; simpl_sum_l. apply xif_idem. rewrite <- IHk. destruct b; auto with algebra. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph)