proposition: Lemma VLSet_add: forall m q, equal (VLSet_to_X (VLSet.add m q)) (plus (VLSet_to_X q) (VLst_to_X m)).
proof: Proof. induction q as [|q1 q2 IH z Hz Hq] using VLSetProps.P.set_induction; unfold VLSet_to_X. rewrite (VLSetProps.P.fold_add _ Hpc Hpt) by setdec. rewrite VLSetProps.P.fold_1b by assumption. unfold fplus; simpl. symmetry. constructor. destruct (VLSetProps.P.In_dec m q2) as [Hn|Hn]. rewrite (VLSetProps.add_fold _ Hpc _ Hn). rewrite <- (VLSetProps.P.fold_equal _ Hpc Hpt _ (VLSetProps.P.add_remove Hn)). rewrite (VLSetProps.P.fold_add _ Hpc Hpt). unfold fplus. destruct_tests; auto. rewrite <- plus_assoc, plus_idem; reflexivity. setdec. rewrite (VLSetProps.P.fold_add _ Hpc Hpt _ Hn). unfold fplus. destruct_tests; auto. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)