more precise and complete transitive closure of proven_classrel, using existing Sorts.classes_of which is already closed; transfer theorems where they are picked from the theory; tuned;