fact: Fixpoint clean1 (x: X): X := match x with | dot x y => let x := clean1 x in let y := clean1 y in if is_one x then y else if is_one y then x else dot x y | plus x y => plus (clean1 x) (clean1 y) | x => x end.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)