fact: Definition class_of' (t : T) x := NumMap.fold (fun a b acc => if fst (equiv t x a) && fst (equiv t x b) then (NumSet.add a (NumSet.add b acc)) else acc ) (p t) NumSet.empty.
imports: ATBR(Common) ATBR(MyFSets) ATBR(BoolView) ATBR(Numbers)