proposition: Lemma Is_one t : is_one t = true -> t = one.
proof: Proof. destruct t; simpl; intuition discriminate. Qed.
imports: ATBR(MyFSets MyFSetProperties) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(Numbers) ATBR(Reification)