hard create-theorem