proposition: Lemma VLst_to_X_compat: forall i j, VLst.eq i j -> equal (VLst_to_X i) (VLst_to_X j).
proof: Proof. unfold VLst_to_X. intros i j H. apply VLstA.reflect in H. subst. reflexivity. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)