I want to share this live playground for FOL, an old system from the late 70s. It has many precursor ideas about reasoning at the meta-level, including the now common proof by reflection which turns proving in the object theory into evaluation in the meta theory, and is common in Rocq, Lean, and other proof assistants.