added thms to perm_compose (so far only composition theorems were included where the type of the permutation was equal)

tuned one comment

fixed a bug that occured when more than one atom-type is declared.

fixed proof

more cleaning up - this time of the cp-instance proofs

improved the finite-support proof added finite support proof for options (I am surprised that one does not need more fs-proofs; at the moment only lists, products, units and atoms are shown to be finitely supported (of course also every nominal datatype is finitely supported)) deleted pt_bool_inst - not necessary because discrete types are treated separately in nominal_atoms