proposition: Lemma VLst_add: forall i q, equal (VLst_to_X (List.cons i q)) (dot (VLst_to_X q) (var i)).
proof: Proof. simpl; unfold fdot; intros. destruct_tests; auto. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)