proposition: Lemma functor_sum: forall A B i k f, F A B (sum i k f) == sum i k (fun i => F A B (f i)).
proof: Proof. intros. revert i; induction k; intro i. apply functor_zero. simpl. rewrite functor_plus. apply plus_compat; auto. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(SemiLattice) ATBR(KleeneAlgebra)