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