fact: Fixpoint erase n m (x: X n m): U.X := match x with | dot _ _ _ x y => U.dot (erase x) (erase y) | plus _ _ x y => U.plus (erase x) (erase y) | zero _ _ => U.zero | one _ => U.one | var i => U.var i end.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)