base Card_Equiv_Relations on definitions and proofs in Disjoint_Sets
Created originally on Bitbucket by bulwahn (Lukas Bulwahn)
Was already merged in Bitbucket before import, marked as merged by the import user
This commit bases the Card_Equiv_Relations AFP entry on the recent Isabelle Library Disjoint_Sets. Hence, the two definitions and some previous lemmas are dropped; the remaining lemmas could be also moved to Disjoint_Sets, but this is up to Johannes to decide.