Update defs/lemmas/tactics | New iff levels

Author: Trequetrum

README.md

@@ -1,3 +1,7 @@
+# Lean 4 Logic Game
+
+This is a game about propositional logic as expressed in the Lean Theorem Prover. It uses the [Lean4 Game Engine](https://github.com/leanprover-community/lean4game) and is running live at [adam.math.hhu.de](https://adam.math.hhu.de/#/g/Trequetrum/lean4game-logic)
+
 # A Lean Intro to Logic
 
 Highschool math and zero programming background? Not a problem, the idea of this game is to be extremely approachable. This is a work in progress, so feel free to open an issue to leave feedback of any sort.
@@ -10,4 +14,4 @@ This game is currently in its initial development phase, designed to be largely
 
 While self-contained; in many ways, this game is targeted more at programmers than mathematicians. It doesn't use classical reasoning, sticking instead to constructive logic. The emphasis for most of the theorem proving is on writting proof terms — rather than using tactics. In fact, logic proof automation is such that the tactic **`tauto`** can solve any propositional logic theorem (Though possible, that's an NP-Complete problem).
 
-The main thrust of this game is to create puzzles that are fun to think through on your own. I can write a simple algorithm that solves every proper Sudoku. Yet, when I spend a train-ride scribbling numbers into boxes in my sudoku book, I never lament how much faster my phone's CPU could do the job.
+The main thrust of this game is to create puzzles that are fun to think through on your own.