proposition: Lemma dot_xif_zero: forall b c A B C (x: X A B) (y: X B C), xif b x 0 * xif c y 0 == xif (b&&c) (x*y) 0.
proof: Proof. intros [] []; simpl; trivial with algebra. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)