Which was the first original proof assistant? What was it used for? When and by who was it created? Is it still used today? And what was it's purpose(s)?