fact: Fixpoint size x := (match x with | zero => 1 | one => 1 | var _ => 1 | plus x y => 1 + size x + size y | dot x y => 1 + 2*size x + size y end)%nat.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)