diff --git a/Game.lean b/Game.lean
index 0ea4b16..818cab9 100755
--- a/Game.lean
+++ b/Game.lean
@@ -33,7 +33,7 @@ This introduction as well as some of the tutorial levels can get a bit wordy. Th
 # Building some notation
 Consider the following argument stated in natural language:
 
-“Either cat fur or dog fur was found at the scene of the crime. If dog fur was found at the scene of the crime, Officer Thompson had an allergy attack. If cat fur was found at the scene of the crime, then Macavity is responsible for the crime. But Officer Thompson didn’t have an allergy attack, and so therefore Macavity must be responsible for the crime.” [¹]
+“Either cat fur or dog fur was found at the scene of the crime. If dog fur was found at the scene of the crime, Officer Thompson had an allergy attack. If cat fur was found at the scene of the crime, then Macavity is responsible for the crime. But Officer Thompson didn’t have an allergy attack, and so therefore Macavity must be responsible for the crime.” [[ˢʳᶜ](https://iep.utm.edu/propositional-logic-sentential-logic/#H5)]
 
 Does this argument convince you? The validity of this argument can be made more obvious by representing the chain of reasoning leading from the premises to the conclusion:
 1. Either cat fur was found at the scene of the crime, or dog fur was found at the scene of the crime. (Premise)
@@ -46,9 +46,9 @@ Does this argument convince you? The validity of this argument can be made more
 
 If you take a moment to re-read them again, lines 5, 6, & 7 are all slightly different styles of logical deductions.
 
-- Line 5 is deducing the negation of the left-hand side of an \"if ... then ...\" statement. Just for references' sake, we'll give this style of reasoning a name: **modus tollens** (Feel free to search that name ☺ )
-- Line 6 is using the process of elimination on two options. This is the style of reasoning responsible for Sherlock Holmes' most famous quote — \"When you have eliminated the impossible, whatever remains, however improbable, must be the truth\". We'll give this a name too: **modus tollendo ponens**
-- Line 7 is the conclusion and is applying the \"if ... then ...\" statement on line 3. We'll call this one **modus ponens**.
+- Line 5 is deducing the negation of the left-hand side of an \"if ... then ...\" statement. Just for references' sake, we'll give this style of reasoning a name: [**modus tollens**](https://en.wikipedia.org/wiki/Modus_tollens)
+- Line 6 is using the process of elimination on two options. This is the style of reasoning responsible for Sherlock Holmes' most famous quote — \"When you have eliminated the impossible, whatever remains, however improbable, must be the truth\". We'll give this a name too: [**modus tollendo ponens**](https://en.wikipedia.org/wiki/Modus_ponendo_tollens)
+- Line 7 is the conclusion and is applying the \"if ... then ...\" statement on line 3. We'll call this one [**modus ponens**](https://en.wikipedia.org/wiki/Modus_ponens).
 
 We won't always be denoting these with Latin names, but the general process of being able to give some generically useful deductive reasoning a name is nice. It makes them easier to reference. During the course of this game some of your proofs will be given names and correspondingly unlocked in your inventory. Thus names are a way to avoid proving the same thing over and over again.
 
@@ -119,7 +119,7 @@ Click on the first world — **Party Invites** — to get started.
 
 ----
 
-[¹]Logic example taken from [IEP](https://iep.utm.edu/propositional-logic-sentential-logic/#H5) entry: *Propositional Logic*.
+[ˢʳᶜ]Logic example taken from [IEP](https://iep.utm.edu/propositional-logic-sentential-logic/#H5) entry: *Propositional Logic*.
 "
 
 Info "
diff --git a/Game/Doc/Definitions.lean b/Game/Doc/Definitions.lean
index e3bb02d..1f878c5 100755
--- a/Game/Doc/Definitions.lean
+++ b/Game/Doc/Definitions.lean
@@ -2,39 +2,11 @@ import GameServer.Commands
 
 namespace GameLogic
 
-def and_left {P Q : Prop} (h : P ∧ Q) : P := And.left h
-
-DefinitionDoc GameLogic.and_left as "∧ elim left" "
-# ∧ Elimination Left
-### and_left : P ∧ Q -> P`
-
-If `h` is a term with a type like `AP∧ Q`
-
-`and_left h`, `h.left` or `h.1` are all expressions for denoting the left-hand side of the given evidence. In this case, the left side has a type of `P`.
-"
-
-def and_right {P Q : Prop} (h : P ∧ Q) : Q := And.right h
-
-DefinitionDoc GameLogic.and_right as "∧ elim right" "
-# ∧ Elimination Right
-### and_right : P ∧ Q -> Q`
-
-If `h` is a term with a type like `P ∧ Q`
-
-`and_right h`, `h.right` or `h.2` are all expressions for denoting the right-hand side of the given evidence. In this case, the left side has a type of `Q`.
-"
-
-def and_intro {P Q : Prop} (left : P) (right : Q) : P ∧ Q := And.intro left right
-
-DefinitionDoc GameLogic.and_intro as "∧ intro" "
-# and_intro
-### `and_intro : P -> Q -> P ∧ Q`
-`and_intro` is a function with two parameters. It takes two disparate pieces of evidence and combines them into a single piece of evidence. If `(e₁ : P)` and `(e₂ : Q)` are evidence, then
-```
-have h : P ∧ Q := and_intro e₁ e₂
-```
-## Auxilliary:
-Since this is done so often, here are a whole handfull of ways to combine evidence. They all build the same conjunction in the end, so you can use whichever suits you.
+DefinitionDoc GameLogic.and_def as "∧" "
+# Conjunction
+## Introduction
+An “And” can be introduced with the `and_intro` theorem. Conjunctions and biconditionals can both be constructed using the angle bracket notation as well.
+### Examples
 ```
 -- Assumptions
 p : P
@@ -43,15 +15,66 @@ q : Q
 -- Explicit Constructer, no annotations needed
 have h₁ := and_intro p q
 have h₂ := and_intro (left := p) (right := q)
--- Implicit Structure, annotations based on context
-have h₃ : P ∧ Q := {left := p, right := q}
-have h₄ := ({left := p, right := q} : P ∧ Q)
-have h₅ := {left := p, right := q : P ∧ Q}
 -- Implicit Constructuer, annotations based on context
 -- Type these angle brackets with “\\<” and “\\>”
 have h₆ : P ∧ Q := ⟨p,q⟩
 have h₇ := (⟨p,q⟩ : P ∧ Q)
 ```
+## Elimination
+An “And” like `h : P ∧ Q` can be reduced in two ways:
+1. Aquire evidence for `P` using `and_left h` or `h.left`
+2. Aquire evidence for `Q` using `and_right` or `h.right`
+"
+
+DefinitionDoc GameLogic.or_def as "∨" "
+# Disjunction
+## Introduction
+An “Or” like `h : P ∨ Q` can be introduced in two ways:
+1. If you have `p : P`, you can use `or_inl p`
+2. If you have `q : Q`, you can use `or_inr q`
+
+In either case, remember that the other type in your disjunction must be inferable in context or supplied as part of the expression. For example: `(or_inl p : P ∨ Q)`
+## Elimination
+An “Or” like `h : P ∨ Q` can be be eliminated if both P and Q imply the same proposition. In this example, P or Q implies R:
+```
+-- Assumptions
+pvq: P ∨ Q
+pr : P → R
+qr : Q → R
+-- Goal: R
+exact or_elim pvq pr qr
+```
+"
+
+DefinitionDoc GameLogic.false_def as "False" "
+# False
+This is a proposition for which there can never be any evidence. If your assumptions lead you to evidence for `False`, then your assumptions are inconsitent and you can use `false_elim` to deduce any proposition you like.
+"
+
+DefinitionDoc GameLogic.iff_def as "↔" "
+# Biconditional
+## Introduction
+An “If and only if” can be introduced with the `iff_intro` theorem. Biconditionals and conjunctions can both be constructed using the angle bracket notation as well.
+### Examples
+```
+-- Assumptions
+h₁ : P → Q
+h₂ : Q → P
+-- Each new term is evidence for P ↔ Q
+-- Explicit Constructer, no annotations needed
+have h₁ := iff_intro h₁ h₂
+have h₂ := iff_intro (mp := h₁) (mpr := h₂)
+-- Implicit Constructuer, annotations based on context
+-- Type these angle brackets with “\\<” and “\\>”
+have h₆ : P ↔ Q := ⟨h₁, h₂⟩
+have h₇ := (⟨h₁, h₂⟩ : P ↔ Q)
+```
+## Elimination
+An “If and only if” like `h : P ↔ Q` can be reduced in two ways:
+1. Aquire evidence for `P → Q` using `iff_mp h` or `h.mp`
+2. Aquire evidence for `Q → P` using `iff_mpr h` or `h.mpr`
+## Rewrite
+Biconditionals let you use the `rewrite` tactic to change goals or assumptions.
 "
 
 DefinitionDoc GameLogic.FunElim as "→ elim" "
@@ -60,7 +83,6 @@ DefinitionDoc GameLogic.FunElim as "→ elim" "
 # Juxtaposition
 Juxtaposition just means “to place next to each other,” which is what we'll do to give a parameter to a function.
 ### Example
-You should already be familiar with `and_intro`. It is a funtion that takes two parameters.
 ```
 -- Assumptions
 e₁ : P
@@ -72,7 +94,6 @@ P ∧ Q
 ```
 exact (and_intro e₁ e₂)
 ```
-Takes `and_intro`, first applies e₂, then second applies e₂.
 ### Example
 ```
 -- Assumptions
@@ -101,9 +122,12 @@ Generally, you don't need to repeat the types when they're obvious from the cont
 # Unicode:
 - `fun` can be written as `λ`
 - `=>` can be written as `↦`
+----
+- `have h₁ : P → P := λp ↦ p`
+- `have h₂ : P ∧ Q → P := λh ↦ h.left`
 "
 
-DefinitionDoc GameLogic.AsciiTable as "Symbol Table" "
+DefinitionDoc GameLogic.AsciiTable as "Unicode Table" "
 ### **Logic Constants & Operators**
 | $Name~~~$ | $Ascii~~~$ | $Unicode$ | $Unicode Cmd$ |
 | --- | :---: | :---: | --- |
@@ -136,6 +160,8 @@ fun h : P ∧ Q => and_intro (and_right h) (and_left h)
 | --- | :---: | --- |
 | Angle brackets | ⟨ ⟩ | `\\<` `\\>` `\\langle` `\\rangle` |
 | Subscript Numbers | ₁ ₂ ₃ ... | `\\1` `\\2` `\\3` ... |
+| Left Arrow | ← | `\\l` `\\leftarrow` `\\gets` `\\<-` |
+| Turnstyle | ⊢ | `\\│-` `\\entails` `\\vdash` `\\goal` |
 "
 
 DefinitionDoc GameLogic.Precedence as "Precedence" "
@@ -195,108 +221,3 @@ Here's a version where you can see it aligned
 (((¬P) ∨ (Q ∧ P)) → Q) ↔ (Q ∨ (R ∨ (¬S)))
 ```
 "
-
-def false_elim {P : Prop} (h : False) : P := h.rec
-
-DefinitionDoc GameLogic.false_elim as "False elim" "
-If
-```
--- Assumptions
-h : False
-```
-then
-```
-have t : T := false_elim h
-```
-will allow you to write any well formed proposition in place of `T`. This makes `false_elim` the \"From `False`, anything goes\" function. **Ex falso quodlibet**.
-"
-
-def or_inl {P Q : Prop} (p : P) : Or P Q := Or.inl p
-
-DefinitionDoc GameLogic.or_inl as "∨ intro left" "
-# Or Introduction Left
-Turns evidence for the lefthand of an `∨` proposition into a disjunction. The context must supply what the righthand side of the disjunction is.
-```
--- Objects
-P Q : Prop
--- Assumptions
-p : P
-```
-allows:
-```
-have h : P ∨ Q := or_inl p
-have h := (or_inl p : P ∨ Q)
-have h := show P ∨ Q from or_inl p
-```
-"
-
-def or_inr {P Q : Prop} (q : Q) : Or P Q := Or.inr q
-
-DefinitionDoc GameLogic.or_inr as "∨ intro right" "
-# Or Introduction Right
-Turns evidence for the righthand of an `∨` proposition into a disjunction. The context must supply what the lefthand side of the disjunction is.
-```
--- Objects
-P Q : Prop
--- Assumptions
-q : Q
-```
-allows:
-```
-have h : P ∨ Q := or_inr q
-have h := (or_inl q : P ∨ Q)
-have h := show P ∨ Q from or_inl q
-```
-"
-
-def or_elim
-  {P Q R : Prop}
-  (h : P ∨ Q)
-  (left : P → R)
-  (right : Q → R) : R :=
-    Or.elim h left right
-
-DefinitionDoc GameLogic.or_elim as "∨ elim" "
-# Or Elimination
-If you can conclude something from `A` and you can conclude the same thing from `B`, then if you know `A ∨ B` it won't matter which of the two happens as you can still guarentee something.
-
-or_elim is also evidence:
-```
-or_elim : (P ∨ Q) → (P → R) → (Q → R) → R`
-```
-# Parameters
-`or_elim` has three parameters:
-1. takes evidence for a disjunction,
-2. evidence an implication on the left,
-3. evidence for an implication on the right.
-# Example
-`or_elim` is your first 3-paramater function.
-```
-pvq: P ∨ Q
-pr : P → R
-qr : Q → R
-have r : R := or_elim pvq pr qr
-```
-"
-
-def iff_intro
-  {P Q : Prop}
-  (hpq: P → Q)
-  (hqp: Q → P) : P ↔ Q :=
-    Iff.intro hpq hqp
-
-DefinitionDoc GameLogic.iff_intro as "↔ intro" "
-  TODO 8888
-"
-
-def iff_mp {P Q : Prop} (h : P ↔ Q) : P → Q := h.mp
-
-DefinitionDoc GameLogic.iff_mp as "↔ elim mp" "
-  TODO 1234
-"
-
-def iff_mpr {P Q : Prop} (h : P ↔ Q) : Q → P := h.mpr
-
-DefinitionDoc GameLogic.iff_mpr as "↔ elim mpr" "
-  TODO 4321
-"
diff --git a/Game/Doc/Lemmas.lean b/Game/Doc/Lemmas.lean
index e1b764d..1ebc713 100755
--- a/Game/Doc/Lemmas.lean
+++ b/Game/Doc/Lemmas.lean
@@ -2,9 +2,143 @@ import GameServer.Commands
 
 namespace GameLogic
 
-def foo_bar(h : α) : α := h
+def and_left {P Q : Prop} (h : P ∧ Q) : P := And.left h
 
-LemmaDoc GameLogic.foo_bar as "fb" in "∩" "TODO"
+LemmaDoc GameLogic.and_left as "and_left" in "∧" "
+# ∧ Elimination Left
+### and_left : P ∧ Q -> P`
+
+If `h` is a term with a type like `AP∧ Q`
+
+`and_left h`, `h.left` or `h.1` are all expressions for denoting the left-hand side of the given evidence. In this case, the left side has a type of `P`.
+"
+
+def and_right {P Q : Prop} (h : P ∧ Q) : Q := And.right h
+
+LemmaDoc GameLogic.and_right as "and_right" in "∧" "
+# ∧ Elimination Right
+### and_right : P ∧ Q -> Q`
+
+If `h` is a term with a type like `P ∧ Q`
+
+`and_right h`, `h.right` or `h.2` are all expressions for denoting the right-hand side of the given evidence. In this case, the left side has a type of `Q`.
+"
+
+def and_intro {P Q : Prop} (left : P) (right : Q) : P ∧ Q := And.intro left right
+
+LemmaDoc GameLogic.and_intro as "and_intro" in "∧" "
+# and_intro
+### `and_intro : P -> Q -> P ∧ Q`
+`and_intro` is a function with two parameters. It takes two disparate pieces of evidence and combines them into a single piece of evidence. If `(e₁ : P)` and `(e₂ : Q)` are evidence, then
+```
+have h : P ∧ Q := and_intro e₁ e₂
+```
+"
+
+def false_elim {P : Prop} (h : False) : P := h.rec
+
+LemmaDoc GameLogic.false_elim as "false_elim" in "¬" "
+If
+```
+-- Assumptions
+h : False
+```
+then
+```
+have t : T := false_elim h
+```
+will allow you to write any well formed proposition in place of `T`. This makes `false_elim` the \"From `False`, anything goes\" function. **Ex falso quodlibet**.
+"
+
+def or_inl {P Q : Prop} (p : P) : Or P Q := Or.inl p
+
+LemmaDoc GameLogic.or_inl as "or_inl" in "∨" "
+# Or Introduction Left
+Turns evidence for the lefthand of an `∨` proposition into a disjunction. The context must supply what the righthand side of the disjunction is.
+```
+-- Objects
+P Q : Prop
+-- Assumptions
+p : P
+```
+allows:
+```
+have h : P ∨ Q := or_inl p
+have h := (or_inl p : P ∨ Q)
+have h := show P ∨ Q from or_inl p
+```
+"
+
+def or_inr {P Q : Prop} (q : Q) : Or P Q := Or.inr q
+
+LemmaDoc GameLogic.or_inr as "or_inr" in "∨" "
+# Or Introduction Right
+Turns evidence for the righthand of an `∨` proposition into a disjunction. The context must supply what the lefthand side of the disjunction is.
+```
+-- Objects
+P Q : Prop
+-- Assumptions
+q : Q
+```
+allows:
+```
+have h : P ∨ Q := or_inr q
+have h := (or_inl q : P ∨ Q)
+have h := show P ∨ Q from or_inl q
+```
+"
+
+def or_elim
+  {P Q R : Prop}
+  (h : P ∨ Q)
+  (left : P → R)
+  (right : Q → R) : R :=
+    Or.elim h left right
+
+LemmaDoc GameLogic.or_elim as "or_elim" in "∨" "
+# Or Elimination
+If you can conclude something from `A` and you can conclude the same thing from `B`, then if you know `A ∨ B` it won't matter which of the two happens as you can still guarentee something.
+
+or_elim is also evidence:
+```
+or_elim : (P ∨ Q) → (P → R) → (Q → R) → R`
+```
+# Parameters
+`or_elim` has three parameters:
+1. takes evidence for a disjunction,
+2. evidence an implication on the left,
+3. evidence for an implication on the right.
+# Example
+`or_elim` is your first 3-paramater function.
+```
+pvq: P ∨ Q
+pr : P → R
+qr : Q → R
+have r : R := or_elim pvq pr qr
+```
+"
+
+def iff_intro
+  {P Q : Prop}
+  (mp: P → Q)
+  (mpr: Q → P) : P ↔ Q :=
+    Iff.intro mp mpr
+
+LemmaDoc GameLogic.iff_intro as "iff_intro" in "↔" "
+  TODO 8888
+"
+
+def iff_mp {P Q : Prop} (h : P ↔ Q) : P → Q := h.mp
+
+LemmaDoc GameLogic.iff_mp as "iff_mp" in "↔" "
+  TODO 1234
+"
+
+def iff_mpr {P Q : Prop} (h : P ↔ Q) : Q → P := h.mpr
+
+LemmaDoc GameLogic.iff_mpr as "iff_mpr" in "↔" "
+  TODO 4321
+"
 
 def modus_ponens {P Q : Prop} (hpq: P → Q) (p: P) : Q := hpq p
 
@@ -33,7 +167,7 @@ There is are infix operators for function application; they look like `|>` and `
 
 `<|` parses `x` with lower precedence, which means that `f <| g $ <|` is interpreted as `(f (g x))` rather than `((f g) x)`.
 
-It's twin, `|>` chains such that x |> f |> g is interpreted as g (f x).
+It's twin, `|>` chains such that `x |> f |> g` is interpreted as `g (f x)`.
 
 What makes the infix operators usefull is that they can often replace a pair of brackets `(...)` making expressions easier to read.
 "
@@ -43,7 +177,7 @@ def and_comm {P Q : Prop}: P ∧ Q ↔ Q ∧ P :=
     λ⟨l,r⟩ ↦ ⟨r,l⟩
   ⟩
 
-LemmaDoc GameLogic.and_comm as "and_comm" in "↔" "
+LemmaDoc GameLogic.and_comm as "and_comm" in "∧" "
 # ∧ is commutative
 
 `and_comm` is evidence that `P ∧ Q ↔ Q ∧ P`
@@ -54,12 +188,18 @@ def and_assoc {P Q R : Prop}: P ∧ Q ∧ R ↔ (P ∧ Q) ∧ R :=
     λ⟨⟨p,q⟩,r⟩ ↦ ⟨p,q,r⟩
   ⟩
 
+LemmaDoc GameLogic.and_assoc as "and_assoc" in "∧" "
+# ∧ is Associative
+
+`and_assoc` is evidence that `P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R`
+"
+
 def or_comm {P Q : Prop}: P ∨ Q ↔ Q ∨ P :=
   ⟨ (Or.elim · Or.inr Or.inl),
     (Or.elim · Or.inr Or.inl)
   ⟩
 
-LemmaDoc GameLogic.or_comm as "or_comm" in "↔" "
+LemmaDoc GameLogic.or_comm as "or_comm" in "∨" "
 # ∨ is commutative
 
 `or_comm` is evidence that `P ∨ Q ↔ Q ∨ P`
@@ -98,6 +238,12 @@ example {P Q R : Prop}: P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R := by
     (Or.inr ∘ Or.inr))
   exact ⟨mp,mpr⟩
 
+LemmaDoc GameLogic.or_assoc as "or_assoc" in "∨" "
+# ∨ is Associative
+
+`or_assoc` is evidence that `P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R`
+"
+
 def imp_trans {P Q R : Prop} (hpq : P → Q) (hqr : Q → R) (p : P): R := hqr (hpq p)
 
 LemmaDoc GameLogic.imp_trans as "imp_trans" in "→" "
@@ -123,7 +269,7 @@ def not_not_not {P : Prop}: ¬¬¬P ↔ ¬P := ⟨
   (λnp nnp ↦ nnp $ np)
 ⟩
 
-LemmaDoc GameLogic.not_not_not as "not_not_not" in "↔" "
+LemmaDoc GameLogic.not_not_not as "not_not_not" in "↔ extra" "
 # Negation is stable
 A nice result of this theorem is that any more than 2 negations can be simplified down to 1 or 2 negations.
 ```
@@ -131,11 +277,11 @@ not_not_not : ¬¬¬P ↔ ¬P
 ```
 "
 
-def mt {P Q : Prop} (h: P → Q) (nq: ¬Q) : ¬P := h ≫ nq
+def modus_tollens {P Q : Prop} (h: P → Q) (nq: ¬Q) : ¬P := h ≫ nq
 
-LemmaDoc GameLogic.mt as "mt" in "→" "
+LemmaDoc GameLogic.modus_tollens as "modus_tollens" in "→" "
 # Modus Tollens
-Denying the consequent. We've given this theorem an extra short name because it appears so often.
+Denying the consequent.
 
 If P, then Q.\\
 Not Q.\\
@@ -145,7 +291,7 @@ mt : (P → Q) → ¬Q → ¬P
 ```
 
 ### Infix Operator:
-`mt` is a specialized version of `imp_trans`, which makes it possible to use `≫` as an infix operator for `mt`.
+`modus_tollens` is a specialized version of `imp_trans`, which makes it possible to use `≫` (which is written as “`\\gg`”) as an infix operator for `modus_tollens`.
 "
 
 def identity {P : Prop}(p : P) : P := p
diff --git a/Game/Doc/Tactics.lean b/Game/Doc/Tactics.lean
index af8d216..2e24e6a 100755
--- a/Game/Doc/Tactics.lean
+++ b/Game/Doc/Tactics.lean
@@ -94,24 +94,23 @@ Goal:
 TacticDoc rw "
 ## Summary
 
-If `h` is a proof of an equality `X = Y`, then `rw [h]` will change
-all `X`s in the goal to `Y`s. It's the way to \"substitute in\".
+If `h₁` is a proof of an equivalence `P ↔ Q`, then `rw [h₁]` will change
+all `P`s in the goal to `Q`s. It's the way to “substitute in”.
 
 ## Variants
 
-* `rw [← h]` (changes `Y`s to `X`s; get the back arrow by typing `\\left ` or `\\l`.)
+* `rw [← h₁]` — changes `Q`s to `P`s; get the back arrow by typing `\\left ` or `\\l`.
 
-* `rw [h1, h2]` (a sequence of rewrites)
+* `rw [h₁, h₂, h₃, h₄]` — a sequence of rewrites
 
-* `rw [h] at h2` (changes `X`s to `Y`s in hypothesis `h2`)
+* `rw [h₁] at h₂` — changes `P`s to `Q`s in hypothesis `h₂`
 
-* `rw [h] at h1 h2 ⊢` (changes `X`s to `Y`s in two hypotheses and the goal;
-get the `⊢` symbol with `\\|-`.)
+* `rw [h₁] at h₂ h₃ ⊢` — changes `X`s to `Y`s in two hypotheses and the goal;
+get the `⊢` symbol with `\\|-`.
 
-* `repeat rw [add_zero]` will keep changing `? + 0` to `?`
-until there are no more matches for `? + 0`.
+* `repeat rw [h₁]` — keep attempting to `rw` until there are no more matches. For example, if the goal is `¬¬¬¬¬¬¬¬¬¬¬¬¬¬¬¬¬¬¬P` you can use `rw [not_not_not]` 9 times or just use `repeat rw [not_not_not]` once to get `¬P`
 
-* `nth_rewrite 2 [h]` will change only the second `X` in the goal to `Y`.
+* `nth_rewrite 2 [h₁]` — will change only the second `P` in the goal to `Q`.
 "
 
 TacticDoc «repeat» "
diff --git a/Game/Levels/AndIntro/L01.lean b/Game/Levels/AndIntro/L01.lean
index 0b82d1c..c4cebfe 100755
--- a/Game/Levels/AndIntro/L01.lean
+++ b/Game/Levels/AndIntro/L01.lean
@@ -7,7 +7,7 @@ Level 1
 Title "Exactly! It's in the premise"
 
 NewTactic exact
-NewDefinition GameLogic.AsciiTable
+NewDefinition GameLogic.AsciiTable GameLogic.and_def
 
 Introduction "
 # Introduction
diff --git a/Game/Levels/AndIntro/L02.lean b/Game/Levels/AndIntro/L02.lean
index 82fef46..0ce680d 100755
--- a/Game/Levels/AndIntro/L02.lean
+++ b/Game/Levels/AndIntro/L02.lean
@@ -6,23 +6,23 @@ World "AndIntro"
 Level 2
 Title "And Introduction"
 
-NewDefinition GameLogic.and_intro
+NewLemma GameLogic.and_intro
 
 Introduction "
 # Sending Invitations in a Single Package
-You have two letters, one extending an invitation to Paul and the other to Sarah. Since they share a residence, you'd like to consolidate their invites into a single package for shipping. The box you're using has space for two items, one on the left and one on the right.\\
+You have two letters, one extending an invitation to Pippin and the other to Sybeth. Since they share a residence, you'd like to consolidate their invites into a single package for shipping. The box you're using has space for two items, one on the left and one on the right.\\
 \\
-You've labelled the box explicitly, specifying that Paul's invitation is on the left and Sarah's invitation is on the right. This ensures there's no confusion about the contents of the box. Upon opening it, they will easily locate their respective invites without the need to search the entire package.
+You've labelled the box explicitly, specifying that Pippin's invitation is on the left and Sybeth's invitation is on the right. This ensures there's no confusion about the contents of the box. Upon opening it, they will easily locate their respective invites without the need to search the entire package.
 # Proposition Key:
-- P — “**P**aul is invited to the party”
-- S — “**S**arah is invited to the party”
+- P — “**P**ippin is invited to the party”
+- S — “**S**ybeth is invited to the party”
 # `∧`
 The hat symbol “ ∧ ” is how logicians denote a conjunction — a logical “and”. `A ∧ B` means “A and B”. It works the way you would intuitively expect. Like a lot of math operators (`+,-,÷,×`,and others), the `∧` symbol is an infix operator. This means it has a left side and a right side. Looking at `A ∧ B`, you can see that `A` is on the left and `B` is on the right.\\
 \\
 In this game, that means anything operating as evidence for `A ∧ B` will have a left part and a right part as well. The box described in the intro works this way.
 # Assumptions
-- `p : P` — Your invitation for Paul is evidence that Paul is invited to the party
-- `s : S` — Your invitation for Sarah is evidence that Sarah is invited to the party
+- `p : P` — Your invitation for Pippin is evidence that Pippin is invited to the party
+- `s : S` — Your invitation for Sybeth is evidence that Sybeth is invited to the party
 # Goal
 Use `p` and `s` to produce evidence that `P ∧ S`. Remember that you use evidence (generally lowercase letters), to deduce new propositions (generally uppercase letters)
 
@@ -41,7 +41,7 @@ Statement (P S : Prop)(p: P)(s : S) : P ∧ S := by
 
 
 Conclusion "
-You've got evidence that Paul and Sarah are invited to the party.\\
+You've got evidence that Pippin and Sybeth are invited to the party.\\
 \\
 Here are some answers the game would have accepted:
 ```
diff --git a/Game/Levels/AndIntro/L03.lean b/Game/Levels/AndIntro/L03.lean
index e7aaa2c..98afb8b 100755
--- a/Game/Levels/AndIntro/L03.lean
+++ b/Game/Levels/AndIntro/L03.lean
@@ -11,17 +11,17 @@ NewTactic «have»
 
 Introduction "
 # Too Many Invites
-You have invites for Jason, Justin, Jaime, and Jordan who all live together. Unfortunately, boxes only have space for two items, but you've thought up a clever solution!
-1. You'll put Jason's and Jaime's invites in a box,
-2. You'll put Jordan's and Justin's invites in another box.
+You have invites for Alarfil, Ilyn, Orin, and Uriel who all live together. Unfortunately, boxes only have space for two items, but you've thought up a clever solution!
+1. You'll put Alarfil's and Ilyn's invites in a box,
+2. You'll put Orin's and Uriel's invites in another box.
 3. You'll put both boxes in a final box.
 ### Nested Boxes!
 Nesting boxes like this is a way to get around the “two items per box” rule. Ensure that everything is correctly labelled to guarantee each invite reaches the correct recipient.
 # Proposition Key:
-- A — J**a**son is invited to the party
-- I — Ja**i**me is invited to the party
-- O — J**o**rdan is invited to the party
-- U — J**u**stin is invited to the party
+- A — **A**larfil is invited to the party
+- I — **I**lyn is invited to the party
+- O — **O**rin is invited to the party
+- U — **U**riel is invited to the party
 
 
 # The `have` Tactic
@@ -59,10 +59,10 @@ Great! Another 4 invites sent out. You're getting the hang of this.
 
 ----
 ````
--- 1. Jason and Jaime: A ∧ I
+-- 1. Alarfil and Ilyn: A ∧ I
 have h₁ := and_intro a i
 
--- 2. Jordan and Justin: O ∧ U
+-- 2. Orin and Uriel: O ∧ U
 have h₂ := and_intro o u
 
 -- 3. both boxes in a final box
diff --git a/Game/Levels/AndIntro/L04.lean b/Game/Levels/AndIntro/L04.lean
index 7140a82..0d67a52 100755
--- a/Game/Levels/AndIntro/L04.lean
+++ b/Game/Levels/AndIntro/L04.lean
@@ -6,20 +6,20 @@ World "AndIntro"
 Level 4
 Title "And Elimination"
 
-NewDefinition GameLogic.and_left
+NewLemma GameLogic.and_left
 
 Introduction "
 # Using Only What Is Needed
-Sarah has left a voicemail on your answering machine. In it she says “Hello, it's Sarah, I'm calling to confirm that Paul is coming to the party and I am also coming to the party! See you then!”\\
+Sybeth has left a voicemail on your answering machine. In it she says “Hello, it's Sybeth, I'm calling to confirm that Pippin is coming to the party and I am also coming to the party! See you then!”\\
 \\
-You'd like to convince Alan to join the party. You know that Alan is good friends with Paul. Constructing evidence that Paul is attending the party might just be the key to convincing Alan to join as well.
+You'd like to convince Cyna to join the party. You know that Cyna is good friends with Pippin. Constructing evidence that Pippin is attending the party might just be the key to convincing Cyna to join as well.
 # Proposition Key:
-- P — \"**P**aul is coming to the party\"
-- S — \"**S**arah is coming to the party\"
+- P — \"**P**ippin is coming to the party\"
+- S — \"**S**ybeth is coming to the party\"
 # Assumptions:
 - `h : P ∧ S` — The voicemail (`h`) is evidence that `P ∧ S`
-# Convincing Alan
-Alan is close with Paul, but you don't know much about his friendship with Sarah. You want only a relevant part of the voicemail. Fortunately, you know that any evidence with an `∧` has a left part and a right part. You can use this knowledge to pull evidence out of `h`.\\
+# Convincing Cyna
+Cyna is close with Pippin, but you don't know much about his friendship with Sybeth. You want only a relevant part of the voicemail. Fortunately, you know that any evidence with an `∧` has a left part and a right part. You can use this knowledge to pull evidence out of `h`.\\
 \\
 This can be done with either of these two methods:
 ```
@@ -29,13 +29,13 @@ have p := and_left h
 Once you've done this, you're very close to level 1 again where the Goal is directly in your assumptions.
 "
 
-/-- Exhibit evidence that Paul is coming to the party. -/
+/-- Exhibit evidence that Pippin is coming to the party. -/
 Statement (P S : Prop)(h: P ∧ S) : P := by
   have p := h.left
   exact p
 
 Conclusion "
-You've got a proof that Paul is coming to the party! Lets see if Alan will attend as well.
+You've got a proof that Pippin is coming to the party! Lets see if Cyna will attend as well.
 
 ----
 Which proof did you use?
diff --git a/Game/Levels/AndIntro/L05.lean b/Game/Levels/AndIntro/L05.lean
index 82cd421..d48d087 100755
--- a/Game/Levels/AndIntro/L05.lean
+++ b/Game/Levels/AndIntro/L05.lean
@@ -6,7 +6,7 @@ World "AndIntro"
 Level 5
 Title "And Elimination 2"
 
-NewDefinition GameLogic.and_right
+NewLemma GameLogic.and_right
 
 Introduction "
 # Another Unlock
diff --git a/Game/Levels/AndIntro/L06.lean b/Game/Levels/AndIntro/L06.lean
index 3e5bf59..6b8d59a 100755
--- a/Game/Levels/AndIntro/L06.lean
+++ b/Game/Levels/AndIntro/L06.lean
@@ -8,12 +8,12 @@ Title "Mix and Match"
 
 Introduction "
 # Mixed Up Conjunctions
-Recall when you placed the invites for Jason, Justin, Jaime, and Jordan in separate boxes. There was a mix-up in the arrangement. Can you fix it so that Jason and Justin's invites are together?
+Recall when you placed the invites for Alarfil, Ilyn, Orin, and Uriel in separate boxes. There was a mix-up in the arrangement. Can you fix it so that Alarfil and Uriel's invites are together?
 # Proposition Key:
-- A — J**a**son is invited to the party
-- I — Ja**i**me is invited to the party
-- O — J**o**rdan is invited to the party
-- U — J**u**stin is invited to the party
+- A — **A**larfil is invited to the party
+- I — **I**lyn is invited to the party
+- O — **O**rin is invited to the party
+- U — **U**riel is invited to the party
 ### Quick tip!
 You can type h₁ by entering \"h\\1\". There's symbol table for all the unicode shortcuts this game uses. It should be available under **Definitions** in your inventory.
 "
diff --git a/Game/Levels/AndIntro/L08.lean b/Game/Levels/AndIntro/L08.lean
index cd2e69f..8f3b5a8 100755
--- a/Game/Levels/AndIntro/L08.lean
+++ b/Game/Levels/AndIntro/L08.lean
@@ -14,21 +14,21 @@ Using the `have` tactic, you can break this task down into digestible chunks. Th
 # Rearranging Boxes
 Finally, a bunch of your invites have returned with RSVPs. The mailman has delivered them in a big box. Make a list of the expected attendees so far.
 # Proposition Key:
-- A — J**a**son is coming to the party
-- I — Ja**i**me is coming to the party
-- L — A**l**an is coming to the party
-- O — J**o**rdan is coming to the party
-- P — **P**aul is coming to the party
-- S — **S**arah is coming to the party
-- U — J**u**stin is coming to the party
+- A — **A**larfil is coming to the party
+- C — **C**yna** is coming to the party
+- I — **I**lyn** is coming to the party
+- O — **O**rin** is coming to the party
+- P — **P**ippin** is coming to the party
+- S — **S**ybeth** is coming to the party
+- U — **U**riel** is coming to the party
 "
 
 /-- Take apart and build evidence -/
-Statement (A I L O P S U : Prop)(h: ((P ∧ S) ∧ A) ∧ ¬I ∧ (L ∧ ¬O) ∧ ¬U) : A ∧ L ∧ P ∧ S := by
+Statement (A C I O P S U : Prop)(h: ((P ∧ S) ∧ A) ∧ ¬I ∧ (C ∧ ¬O) ∧ ¬U) : A ∧ C ∧ P ∧ S := by
   have psa := h.left
-  have l := h.right.right.left.left
-  have lps := and_intro l psa.left
-  exact and_intro psa.right lps
+  have c := h.right.right.left.left
+  have fps := and_intro c psa.left
+  exact and_intro psa.right fps
 
 Conclusion "
 Amazing! You've mastered \"AND\".
diff --git a/Game/Levels/ExSyl.lean b/Game/Levels/ExSyl.lean
index 253e43a..dd4a152 100755
--- a/Game/Levels/ExSyl.lean
+++ b/Game/Levels/ExSyl.lean
@@ -5,6 +5,16 @@
 -- import Game.Doc.Definitions
 -- import Game.Doc.Tactics
 
+-- Paul ↦ Pippin
+-- Sarah ↦ Sybeth
+-- Jason ↦ Alarfil
+-- Jaime ↦ Ilyn
+-- Jordan ↦ Orin
+-- Justin ↦ Uriel
+-- Alan ↦ Fredu ↦ Cyna
+-- Robbie ↦ Riffin
+-- Bella ↦ Bella
+-- Bert ↦ Lippa
 
 theorem imp_imp_imp {a b c d : Prop} (h₀ : c → a) (h₁ : b → d) : (a → b) → (c → d) := (h₁ ∘ · ∘ h₀)
 
diff --git a/Game/Levels/IffIntro.lean b/Game/Levels/IffIntro.lean
index 8b607d3..dde3540 100644
--- a/Game/Levels/IffIntro.lean
+++ b/Game/Levels/IffIntro.lean
@@ -1,10 +1,15 @@
 import Game.Levels.IffIntro.L01
 import Game.Levels.IffIntro.L02
+import Game.Levels.IffIntro.L03
+import Game.Levels.IffIntro.L04
 
 World "IffIntro"
-Title "↔ Tutorial"
+Title "↔ Tutorial: Party Games"
 
 Introduction "
+# Party Games
+A soirée requires a diligent and clear-headed host if the guests are to have fun. It's your job to ensure everybody is having a good time. Let the games begin!
+
 # Propositional Equivalence
 ## Biconditional: If and only if
 The `↔` operator doesn't introduce anything new. `P ↔ Q` can be constructed whenever evidence for both `P → Q` and `Q → P` is available. In general, if `h₁` and `h₂` are evidence as follows:
diff --git a/Game/Levels/IffIntro/L01.lean b/Game/Levels/IffIntro/L01.lean
index d454438..90757fa 100755
--- a/Game/Levels/IffIntro/L01.lean
+++ b/Game/Levels/IffIntro/L01.lean
@@ -8,14 +8,15 @@ Title "Iff_Intro"
 
 NewTactic rw
 NewHiddenTactic «repeat» nth_rewrite
-NewDefinition GameLogic.iff_intro
+NewLemma GameLogic.iff_intro
+NewDefinition GameLogic.iff_def
 
 Introduction "
 # Coupled Conditionals
-Sarah and Jason are a couple. In effect, this means that if Sarah is attending the party, then Jason is attending and vise versa. Therefore Sarah is attending if and only if Jason is attending.
+Sybeth and Alarfil are a couple. In effect, this means that if Sybeth is playing a party game, then Alarfil is playing too and vise versa. Therefore Sybeth is playing Charades if and only if Alarfil playing.
 # Proposition Key:
-- J — Jason is attending
-- S — Sarah is attending
+- J — Alarfil is playing Charades
+- S — Sybeth is playing Charades
 # Unlocked `↔ intro`
 Assuming `e₁ : P → Q` and `e₂ : Q → P`, you can introduce a biconditional with `have h := iff_intro e₁ e₂`, though the anonymous constructor syntax works just like it does for conjunctions: `have h : P ↔ Q := ⟨e₁, e₂⟩`
 "
diff --git a/Game/Levels/IffIntro/L02.lean b/Game/Levels/IffIntro/L02.lean
index 2f43f86..8bc6abd 100644
--- a/Game/Levels/IffIntro/L02.lean
+++ b/Game/Levels/IffIntro/L02.lean
@@ -4,17 +4,19 @@ open GameLogic
 
 World "IffIntro"
 Level 2
-Title "Title"
+Title "Conjuctive Iff"
 
-NewDefinition GameLogic.iff_mp GameLogic.iff_mpr
+NewLemma
+  GameLogic.iff_mp
+  GameLogic.iff_mpr
 
 Introduction "
 # Two sides to every coin
-You're flipping a coin to decide what color placemats you you want. Heads means blue placemats and tails means purple placemats. Here's the thing, you're secretly hoping it comes up blue.
+You're flipping a coin to decide which team gets to guess first in *Salad Bowl*. Heads means blue team and tails means purple team. Even though you're on the purple team, you're secretly hoping it comes up heads.
 # Proposition Key:
-- B — Blue Placemats
-- P — Purple Placemats
-# Unlocked `↔-e mp` and `↔-e mpr`
+- B — Blue Team goes first
+- P — Purple Team goes First
+# Unlocked `iff_mp` and `iff_mpr`
 For a biconditional like `h : P ↔ Q`,
 1. You can extract `P → Q` using `iff_mp h` or `h.mp`. `mp` here is short of modus ponens.
 2. You can extra `Q → P` using `iff_mpr h` or `h.mpr`. `mpr` here is short of modus ponens reversed.
diff --git a/Game/Levels/IffIntro/L03.lean b/Game/Levels/IffIntro/L03.lean
new file mode 100644
index 0000000..2562840
--- /dev/null
+++ b/Game/Levels/IffIntro/L03.lean
@@ -0,0 +1,104 @@
+import Game.Metadata
+
+open GameLogic
+
+World "IffIntro"
+Level 3
+Title "Rewriting"
+
+Introduction "
+# Rewrite the goal
+## To an extreme
+You're playing a round of *The Resistance*. You've been diligently figuring out who is a member of the resistance and who is a spy. It's a bit complicated, but you've reasoned that the current state of affairs is possible if and only if Alarfil and Cyna are members of the resistance and Pippin is a spy. You also know from an earlier reveal that Pippin and Lippa must be on the same team. Therefore, the same argument applies to Lippa as well.
+# Proposition Key:
+- A — Alarfil is a member of the resistance
+- C — Cyna is a member of the resistance
+- L — Lippa is a member of the resistance
+- P — Pippin is a member of the resistance
+# The `rw` tactic
+Depending on the order you've chosen to do the tutorial worlds, you may not yet be familiar with all the symbols in the current proof state. In fact, you may not even have unlocked the tools in your inventory necessary to complete this level. Don't worry, the rewrite tactic makes this level a breeze.\\
+\\
+First, take a look at the proof state and notice that `h₂` and the Goal are extremely similar. In fact, if you replace every occurrence of `L` with `P`, then the two would be identical. That's where `rw` comes in.
+\\
+If you have `hpq : P ↔ Q` then `rw [hpq]` will change all `P`s in the goal to `Q`s. It's the way to “substitute in”.\\
+\\
+The `rw` tactic is an automation tool. It does the rote work of taking apart an expression, looking for a matching sub-expression, swapping in the equivalent sub-expression and then constructing the new equivalent term from there.\\
+\\
+Try it out!
+"
+
+/-- Who is loyal, who is a spy? -/
+Statement
+  (A C L P : Prop)
+  (h₁ : L ↔ P)
+  (h₂ : ¬((A → C ∨ ¬P) ∧ (P ∨ A → ¬C) → (P → C)) ↔ A ∧ C ∧ ¬P)
+  : ¬((A → C ∨ ¬L) ∧ (L ∨ A → ¬C) → (L → C)) ↔ A ∧ C ∧ ¬L := by
+    rw [h₁]
+    exact h₂
+
+example
+  (A C L P : Prop)
+  (h₁ : L ↔ P)
+  (h₂ : ¬((A → C ∨ ¬P) ∧ (P ∨ A → ¬C) → (P → C)) ↔ A ∧ C ∧ ¬P)
+  : ¬((A → C ∨ ¬L) ∧ (L ∨ A → ¬C) → (L → C)) ↔ A ∧ C ∧ ¬L := by
+    rw [← h₁] at h₂
+    exact h₂
+
+example
+  (A C L P : Prop) (h₁ : L ↔ P)
+  (h₂ : ¬((A → C ∨ ¬P) ∧ (P ∨ A → ¬C) → (P → C)) ↔ A ∧ C ∧ ¬P)
+  : ¬((A → C ∨ ¬L) ∧ (L ∨ A → ¬C) → (L → C)) ↔ A ∧ C ∧ ¬L :=
+    ⟨
+      λh₃ ↦ have ⟨a,c,np⟩ := h₂.mp (
+        λh₄ ↦ h₃ (λ⟨hl₅,hr₅⟩ l ↦ h₄ ⟨
+          λa ↦ or_elim
+            (hl₅ a)
+            or_inl
+            (imp_trans h₁.mpr ≫ or_inr)
+        ,
+          λ_ ↦ hr₅ (or_inl l)
+        ⟩ (h₁.mp l))
+      )
+      ⟨a, c, h₁.mp ≫ np⟩
+    ,
+      λ⟨a,c,nl⟩ _ ↦ false_elim (
+        h₂.mpr
+          ⟨a, c, h₁.mpr ≫ nl⟩
+          λ_ _ ↦ c
+      )
+    ⟩
+
+Conclusion "
+Oh, how nice! A fast solution to a complex problem.
+
+----
+If you've read the inventory page for `rw`, you may have seen another solution too. You can use the backwards arrow “`←`” to change `P`s to `L`s instead of `L`s to `P`s. Also, you can change a hypothesis instead of the goal.
+```
+rw [← h₁] at h₂
+exact h₂
+```
+
+Here's an example of what this looks like without the `rw` tactic — if you want to try this solution, copy & paste the following text to the editor input mode.
+```
+exact ⟨
+  λh₃ ↦ have ⟨a,c,np⟩ := h₂.mp (
+    λh₄ ↦ h₃ (λ⟨hl₅,hr₅⟩ l ↦ h₄ ⟨
+      λa ↦ or_elim
+        (hl₅ a)
+        or_inl
+        (imp_trans h₁.mpr ≫ or_inr)
+    ,
+      λ_ ↦ hr₅ (or_inl l)
+    ⟩ (h₁.mp l))
+  )
+  ⟨a, c, h₁.mp ≫ np⟩
+,
+  λ⟨a,c,nl⟩ _ ↦ false_elim (
+    h₂.mpr
+      ⟨a, c, h₁.mpr ≫ nl⟩
+      λ_ _ ↦ c
+  )
+⟩
+```
+The thing to notice here is that this long-form solution needs both `h₁.mp` and `h₁.mpr`. Keep in mind that though it’s often tempting to try to use conditionals (`→`), rewrite **requires** a biconditional (`↔`) to work.
+"
diff --git a/Game/Levels/IffIntro/L04.lean b/Game/Levels/IffIntro/L04.lean
new file mode 100644
index 0000000..6a3e584
--- /dev/null
+++ b/Game/Levels/IffIntro/L04.lean
@@ -0,0 +1,53 @@
+import Game.Metadata
+
+open GameLogic
+
+World "IffIntro"
+Level 4
+Title "Rewriting"
+
+NewLemma
+  GameLogic.and_assoc
+  GameLogic.or_assoc
+
+Introduction "
+# Keep rewriting!
+It's another round of the resistance! This time you know that if you could prove that Alarfil, Cyna, or Lippa are part of the resistance, then that would be good enough to show that least one of the other two are spies.\\
+\\
+It doesn't really matter how your friends are paired up, the same truth will hold.
+# Proposition Key:
+- A — Alarfil is a member of the resistance
+- C — Cyna is a member of the resistance
+- L — Lippa is a member of the resistance
+## new theorems
+Two new theorems have been unlocked for this level. We'll make you prove them later — though I imagine they make a certain amount of intuitive sense regardless.
+1. `or_assoc : P ∨ Q ∨ R ↔ (P ∨ Q) ∨ R`
+2. `and_assoc : P ∧ Q ∧ R ↔ (P ∧ Q) ∧ R`
+"
+
+/-- Exactly 2 rewrites -/
+Statement (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by
+  rw [or_assoc, and_assoc]
+  exact h
+
+example (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by
+  exact imp_trans
+    (λpvqvr ↦ h (or_elim pvqvr
+      (λp ↦ or_inl (or_inl p))
+      (λqvr ↦ or_elim qvr
+        (λq ↦ or_inl (or_inr q))
+        (λr ↦ or_inr r))
+    ))
+    λnpqr pqr ↦ npqr (
+      and_intro (
+        and_intro pqr.left pqr.right.left
+      ) pqr.right.right
+    )
+
+example (P Q R : Prop) (h : (P ∨ Q) ∨ R → ¬((P ∧ Q) ∧ R)) : P ∨ Q ∨ R → ¬(P ∧ Q ∧ R) := by
+  exact or_assoc.mp ≫ h ≫ imp_trans and_assoc.mp
+
+
+Conclusion "
+Onward and upward
+"
diff --git a/Game/Levels/ImpIntro/L01.lean b/Game/Levels/ImpIntro/L01.lean
index a4d1f24..922933b 100755
--- a/Game/Levels/ImpIntro/L01.lean
+++ b/Game/Levels/ImpIntro/L01.lean
@@ -24,25 +24,12 @@ You use an implication the same way you've been using `and_intro`, `and_left`, a
 - have `b : B := h₁ a`
 
 You can read `h₁ a` as modus ponens. In fact, you've unlocked a theorem called modus_ponens that you could use here. Since modus ponens is implemented as function application, you can — and should — always just Juxtapose instead.
-# A retrospective
-You've already been using functions. When you wrote `and_intro p s` in **World 1, Level 2**, you gave the the function `and_intro` two parameters `p : P` and `s : S` and then it returned evidence for `P ∧ S`. \\
-\\
-In World 1, level 7 when you wrote:
-```
-have h₁ := and_left h
-have h₂ := and_right h₁
-have h₃ := and_left h₂
-have h₄ := and_left h₃
-have h₅ := and_right h₄
-exact h₅
--- or
-exact and_right (and_left (and_left (and_right (and_left h))))
--- or
-exact h.left.right.left.left.right
-```
-You were actually treating `and_left` as evidence of `P ∧ Q → P` and you were treating `and_right` as evidence of `P ∧ Q → Q`. Using the game's notation: `and_left : P ∧ Q → P` and `and_right : P ∧ Q → Q`
 # A note
-You'll often see assumptions given one or two letter names (`p`, `r`, `q`, `h₁`, `h₂`, `h₃`, etc). Assumptions are generally not long-lived. They are part of some expression, exhibit some implication, and then are discarded. Their names in this context don't need to be particularly memorable. Theorems — like those on the right side of the game screen — are not fundamentally different from assumptions, but they tend to have longer names because they will be available for all future levels. This level gives an assumption a longer name just for the sake of it.
+You'll often see assumptions given one or two letter names (`p`, `r`, `q`, `h₁`, `h₂`, `h₃`, etc). Assumptions are generally not long-lived. They are part of some expression, exhibit some implication, and then are discarded. Their names in this context don't need to be particularly memorable.\\
+\\
+Theorems — like those on the right side of the game screen — can be thought of as assumptions that are always available for every level (and therefore do not need to be listed under assumptions for any given level). They tend to have longer names because they will be available for all future levels.\\
+\\
+Name-length is not a hard and fast rule, just a common idiom. For a counter-example; this level gives the assumption `bakery_service` a longer name.
 
 # Reminder
 Exhibit evidence for the goal using the `exact` tactic.
diff --git a/Game/Levels/ImpIntro/L02.lean b/Game/Levels/ImpIntro/L02.lean
index 5444841..b4be6ee 100755
--- a/Game/Levels/ImpIntro/L02.lean
+++ b/Game/Levels/ImpIntro/L02.lean
@@ -13,28 +13,35 @@ Introduction "
 There's a show on TV about cake. It asks bakers to distinguish between every-day objects and cakes. This seems silly, because a cake is a cake.
 # Proposition Key:
 - `C` — This object is a Cake
-# Implication \" → \"
+# Implication “ → ”
 You'll notice that this time you don't have any assumptions. Fortunately, `C → C` is a tautology which means you can create an expression for the goal without any assumptions.\\
 \\
-In this game, when you need to show an implication, you write a function. For the function, you can assume the left-hand side of the implication and then potentially use that assumption to exhibit the right-hand side.
+In this game, when you need to show an implication, you write a function. Creating a function requires an assumption and an expression. The assumption is introduced with two parts: `(n : P)` where `n` is any name of your choosing and the `P` is a well formed proposition.\\
+\\
+It looks like this:
 ```
 fun <name> : <Prop> => <expr>
 λ <name> : <Prop> ↦ <expr>
 ```
-In general, you can use whatever you like for the **name** and **proposition**. In this case, you want to show evidence that `C → C`. Below is a hint (just fill in the **expression**):
+Often, when you're writting a function, the game will already know what proposition it's expecting. In such cases, the `<Prop>` becomes an optional part of the function.
+
+# A hint
+Just fill in the `<expr>` below:
 ```
 -- Assuming h is evidence for C,
 -- write an expression for evidence of C
-λ h : C ↦ <expr>
+exact λ h : C ↦ <expr>
 ```
-### Another reminder
-Exhibit evidence using the exact tactic.
 "
 
-/-- Common! Cake is Cake --/
+/-- Common! Cake is Cake -/
 Statement (C: Prop) : C → C := by
   exact λ(h: C) ↦ h
 
+example (C: Prop) : C → C := by
+  exact λh ↦ h
+
+
 Conclusion "
 Once you've gathered evidence confirming that the object is a cake, the game becomes straightforward. The show's appeal lies not in the simple truism that a cake is a cake but rather in the contestants' skill to compile credible evidence. Typically, the most compelling evidence is presented by the host when he cuts into the object, unveiling its contents.
 
diff --git a/Game/Levels/ImpIntro/L04.lean b/Game/Levels/ImpIntro/L04.lean
index 87ca0b2..62430c3 100755
--- a/Game/Levels/ImpIntro/L04.lean
+++ b/Game/Levels/ImpIntro/L04.lean
@@ -10,11 +10,11 @@ NewLemma GameLogic.and_comm
 
 Introduction "
 # A Chain of Reasoning
-You know Jason will be excited about a cake with sprinkles. Since Sarah has just started dating Jason and enjoys seeing him happy, it follows that Sarah will be excited about a cake with sprinkles.
+You know Alarfil will be excited about a cake with sprinkles. Since Sybeth has just started dating Alarfil and enjoys seeing them happy, it follows that Sybeth will be excited about a cake with sprinkles.
 # Proposition Key:
 - `C` — The **C**ake has sprinkles
-- `J` — **J**ason is happy
-- `S` — **S**arah is happy
+- `A` — **A**larfil is happy
+- `S` — **S**ybeth is happy
 
 # Transitivity Aside
 With numbers, if `a` is less than `b` and `b` is less than `c`, then you can deduce that `a` is less than `c`.
@@ -25,11 +25,11 @@ This is the transitive property of `<`. You should be able to show that this sam
 "
 
 /-- Show that → is transitive -/
-Statement (C J S: Prop) (h₁ : C → J) (h₂ : J → S) : C → S := by
+Statement (C A S: Prop) (h₁ : C → A) (h₂ : A → S) : C → S := by
   exact λ(c: C) ↦ h₂ (h₁ c)
 
 -- Example using infix application to drop a pair of brackets.
-example (C J S: Prop) (h₁ : C → J) (h₂ : J → S) : C → S := by
+example (C A S: Prop) (h₁ : C → A) (h₂ : A → S) : C → S := by
   exact λc ↦ h₂ <| h₁ c
 
 Conclusion "
diff --git a/Game/Levels/ImpIntro/L05.lean b/Game/Levels/ImpIntro/L05.lean
index b4b2289..bb756bb 100755
--- a/Game/Levels/ImpIntro/L05.lean
+++ b/Game/Levels/ImpIntro/L05.lean
@@ -4,15 +4,15 @@ open GameLogic
 
 World "ImpIntro"
 Level 5
-Title "Robbie Snacks"
+Title "Riffin Snacks"
 
 NewLemma GameLogic.imp_trans
 
 Introduction "
-# Is Robbie bringing something?
-Robbie is an artsy, but rather eccentric friend of yours.\\
+# Is Riffin bringing something?
+Riffin is an artsy, but rather eccentric friend of yours.\\
 \\
-Ever since you asked Robbie to bring something to your party, he's been sending you rather cryptic emails. Initially, these emails seemed to have nothing to do with the party. However, after receiving the 5th email, you believe you might be able to use them to create evidence that Robbie is bringing something to the party.\\
+Ever since you asked Riffin to bring something to your party, he's been sending you rather cryptic emails. Initially, these emails seemed to have nothing to do with the party. However, after receiving the 5th email, you believe you might be able to use them to create evidence that Riffin is bringing something to the party.\\
 \\
 These are the emails you received:
 1. If you're planning a party then the quest has begun
@@ -28,9 +28,9 @@ You still have your todo list as evidence that you're planning a party. Will it
 - `R` — The **R**oad to victory is long and winding
 - `S` — The **S**tarting gun has fired
 - `T` — It's **T**ime to get serious
-- `U` — Robbie is bringing a **U**nicorn snack
+- `U` — Riffin is bringing a **U**nicorn snack
 # Evidence
-Sometimes visuals can make a logical argument much easier to digest. Here is a diagram you've drawn depicting Robbie's notes so far.
+Sometimes visuals can make a logical argument much easier to digest. Here is a diagram you've drawn depicting Riffin's notes so far.
 $$
 \\begin{CD}
   P  @>{h₁}>> Q       @>{h₂}>> R \\\\
@@ -44,7 +44,7 @@ The Precedence definition page explains that function application is left-associ
 - `((((h₁ h₂) h₃) h₄) h₅)`
 "
 
-/-- Robbie is bringing a unicorn snack -/
+/-- Riffin is bringing a unicorn snack -/
 Statement (P Q R S T U: Prop) (p : P) (h₁ : P → Q) (h₂ : Q → R) (h₃ : Q → T) (h₄ : S → T) (h₅ : T → U) : U := by
   exact (h₁ ≫ h₃ ≫ h₅) p
 
@@ -78,7 +78,7 @@ Conclusion "
 Amazing! He is bringing a snack and you have evidence to prove it too!
 
 ----
-Here are two solutions to Robbie's puzzle. Sometimes it's helpful to see the same puzzles solved in more than one way.
+Here are two solutions to Riffin's puzzle. Sometimes it's helpful to see the same puzzles solved in more than one way.
 ```
 have q := h₁ p
 have t := h₃ q
diff --git a/Game/Levels/ImpIntro/L09.lean b/Game/Levels/ImpIntro/L09.lean
index b2e71a5..8ee7653 100755
--- a/Game/Levels/ImpIntro/L09.lean
+++ b/Game/Levels/ImpIntro/L09.lean
@@ -9,17 +9,17 @@ Title "Uncertain Snacks"
 Introduction "
 # BOSS LEVEL!!!
 # Uncertain Snacks
-Sarah wants to know whether Robbie will still bring a snack, regardless of whether she brings one herself or not.\\
+Sybeth wants to know whether Riffin will still bring a snack, regardless of whether she brings one herself or not.\\
 \\
 She's asked you for evidence that:
-- **If** Robbie is bringing a snack **then**
-  1. Her bringing a snack **implies** Robbie is bringing a snack
-  2. Her not bringing a snack **implies** Robbie is bringing a snack
+- **If** Riffin is bringing a snack **then**
+  1. Her bringing a snack **implies** Riffin is bringing a snack
+  2. Her not bringing a snack **implies** Riffin is bringing a snack
 
 That's a bit convoluted, but you should be able to produce some evidence of this!
 # Proposition Key:
-- `R` — Robbie is bringing a snack
-- `S` — Sarah is bringing a snack
+- `R` — Riffin is bringing a snack
+- `S` — Sybeth is bringing a snack
 "
 
 /-- Write the nessesary nested function(s)! --/
@@ -38,7 +38,7 @@ example (R S : Prop) : R → (S → R) ∧ (¬S → R) := by
   exact λr ↦ ⟨λ_ ↦ r, λ_ ↦ r⟩
 
 Conclusion "
-You're very convincing, and now Sarah can see that if Robbie is bringing a snack, he'll be bringing it regardless of what she does.\\
+You're very convincing, and now Sybeth can see that if Riffin is bringing a snack, he'll be bringing it regardless of what she does.\\
 \\
 On to the next world!
 
diff --git a/Game/Levels/NotIntro/L01.lean b/Game/Levels/NotIntro/L01.lean
index 9c195d5..d9ab8e5 100755
--- a/Game/Levels/NotIntro/L01.lean
+++ b/Game/Levels/NotIntro/L01.lean
@@ -6,6 +6,8 @@ World "NotIntro"
 Level 1
 Title "Not False"
 
+NewDefinition GameLogic.false_def
+
 Introduction "
 # Proof State
 The proof state in the level is as short as you've seen so far. There are no **Objects** or **Assumptions** listed.\\
diff --git a/Game/Levels/NotIntro/L02.lean b/Game/Levels/NotIntro/L02.lean
index 5252c44..5c8d63f 100755
--- a/Game/Levels/NotIntro/L02.lean
+++ b/Game/Levels/NotIntro/L02.lean
@@ -6,14 +6,14 @@ World "NotIntro"
 Level 2
 Title "False implies anything"
 
-NewDefinition GameLogic.false_elim
+NewLemma GameLogic.false_elim
 
 Introduction "
-# Sarah's Punctuality
-Sarah is never on time. Despite her assurances that she'll grace the party with her timely presence, past experiences have proven otherwise. It's almost become a running joke, so much so that you playfully quip, \"Yeah, if you arrive on time, then I'll eat my boots.\"
+# Sybeth's Punctuality
+Sybeth is never on time. Despite her assurances that she'll grace the party with her timely presence, past experiences have proven otherwise. It's almost become a running joke, so much so that you playfully quip, \"Yeah, if you arrive on time, then I'll eat my boots.\"
 # Proposition Key:
 - `B` — You eat your boots
-- `S` — Sarah is on time
+- `S` — Sybeth is on time
 # `false_elim`
 You've unlocked the \"false implies anything\" function. `false_elim` will take evidence for `False` and produce evidence for **anything**.
 # A Tip
diff --git a/Game/Levels/NotIntro/L04.lean b/Game/Levels/NotIntro/L04.lean
index 2acec67..51275e9 100755
--- a/Game/Levels/NotIntro/L04.lean
+++ b/Game/Levels/NotIntro/L04.lean
@@ -8,14 +8,14 @@ Title "Self Contradictory"
 
 Introduction "
 # Self Contradictory
-Jason claims Bert is coming and Alan claims Bert is not coming. They can't both be right.
+Alarfil claims Lippa is coming and Cyna claims Lippa is not coming. They can't both be right.
 # Proposition Key:
-- `B` — Bert is attending the party
+- `L` — **L**ippa is attending the party
 "
 
 /-- The law of non-self-contradiction -/
-Statement (B : Prop) : ¬(B ∧ ¬B) := by
-  exact λ(h : B ∧ ¬B) ↦ h.right h.left
+Statement (L : Prop) : ¬(L ∧ ¬L) := by
+  exact λ(h : L ∧ ¬L) ↦ h.right h.left
 
 Conclusion "
 Well Concluded!
diff --git a/Game/Levels/NotIntro/L05.lean b/Game/Levels/NotIntro/L05.lean
index ce8357d..09b5b6d 100755
--- a/Game/Levels/NotIntro/L05.lean
+++ b/Game/Levels/NotIntro/L05.lean
@@ -8,7 +8,7 @@ Title "Modus Tollens"
 
 Introduction "
 # Modus Tollens
-If Bella comes to the party, she is certain to perform a bawdy song. You've assured Sarah that there will be no bawdy songs at the event. Sarah is disappointed to discover that Bella won't be joining.
+If Bella comes to the party, she is certain to perform a bawdy song. You've assured Sybeth that there will be no bawdy songs at the event. Sybeth is disappointed to discover that Bella won't be joining.
 # Proposition Key:
 - `B` — Bella is attending the party
 - `S` — A bawdy song will be sung
diff --git a/Game/Levels/NotIntro/L06.lean b/Game/Levels/NotIntro/L06.lean
index 2803be4..6f746be 100755
--- a/Game/Levels/NotIntro/L06.lean
+++ b/Game/Levels/NotIntro/L06.lean
@@ -4,23 +4,25 @@ open GameLogic
 
 World "NotIntro"
 Level 6
-Title "Jason"
+Title "Alarfil"
 
-NewLemma GameLogic.mt
+NewLemma GameLogic.modus_tollens
 
 Introduction "
-# The Jason Effect
-You're delighted that Jason will be there.\\
+# The Alarfil Effect
+You're delighted that Alarfil will be there.\\
 \\
-Remarkably, even in moments when Jason lacks humor, he manages to be amusing! His comedic charm persists, regardless of circumstances.
+Remarkably, even in moments when Alarfil lacks humor, he manages to be amusing! His comedic charm persists, regardless of circumstances.
 # Proposition Key:
-- `J` — Jason is humorless
+- `A` — Alarfil is humorless
 "
 
-/-- Remember `h : J → J → False` -/
-Statement (J : Prop) (h: J → ¬J) : ¬J := by
-  exact λ(j : J) ↦ h j j
+/-- Remember `h : A → A → False` -/
+Statement (A : Prop) (h: A → ¬A) : ¬A := by
+  exact λ(a : A) ↦ h a a
 
 Conclusion "
-You're uncertain about the coherence of this, yet it surely must make sense. Let's proceed.
+This joke is a reach, I know, but my answer this this level kinda spells `ahaa` — `λa ↦ h a a`. \\
+\\
+Okay, okay. Let's proceed.
 "
diff --git a/Game/Levels/NotIntro/L09.lean b/Game/Levels/NotIntro/L09.lean
index e024204..6b9fa1a 100755
--- a/Game/Levels/NotIntro/L09.lean
+++ b/Game/Levels/NotIntro/L09.lean
@@ -8,10 +8,10 @@ Title "Implies a Negation"
 
 Introduction "
 # Allergy #1
-Owing to his allergy, if Paul is present, there must be no avocado at the party. Which means that we cannot have both Paul and avacado at the party
+Owing to his allergy, if Pippin is present, there must be no avocado at the party. Which means that we cannot have both Pippin and avacado at the party
 # Proposition Key:
 - `A` — There's avacado at the party
-- `P` — Paul is attending the party
+- `P` — Pippin is attending the party
 "
 
 /-- Show ¬(P ∧ A) -/
diff --git a/Game/Levels/NotIntro/L10.lean b/Game/Levels/NotIntro/L10.lean
index 1fa0daa..af75447 100755
--- a/Game/Levels/NotIntro/L10.lean
+++ b/Game/Levels/NotIntro/L10.lean
@@ -8,10 +8,10 @@ Title "Conjunction Implicaiton"
 
 Introduction "
 # Allergy #2
-We cannot have both Paul and avacado at the party. Which means that if Paul is attending, then there will not be any avacado.
+We cannot have both Pippin and avacado at the party. Which means that if Pippin is attending, then there will not be any avacado.
 # Proposition Key:
 - `A` — There's avacado at the party
-- `P` — Paul is attending the party
+- `P` — Pippin is attending the party
 "
 
 /-- Show P → ¬A. -/
diff --git a/Game/Levels/NotIntro/L11.lean b/Game/Levels/NotIntro/L11.lean
index c9de617..8ff1c1b 100755
--- a/Game/Levels/NotIntro/L11.lean
+++ b/Game/Levels/NotIntro/L11.lean
@@ -8,7 +8,7 @@ Title "not_not_not"
 
 Introduction "
 # Allergy: Triple Confusion
-Paul is allergic to avocado. You tell him you're not *not* **not** bringing avacado!!! Paul gives you a confused look, but after a moment of contemplation, he responds with, \"Ok, good to know.\"
+Pippin is allergic to avocado. You tell him you're not *not* **not** bringing avacado!!! Pippin gives you a confused look, but after a moment of contemplation, he responds with, \"Ok, good to know.\"
 # Proposition Key:
 - `A` — You're bringing avacado
 "
diff --git a/Game/Levels/OrIntro/L01.lean b/Game/Levels/OrIntro/L01.lean
index 0d1ca3b..b4e7128 100755
--- a/Game/Levels/OrIntro/L01.lean
+++ b/Game/Levels/OrIntro/L01.lean
@@ -6,7 +6,8 @@ World "OrIntro"
 Level 1
 Title "Left Evidence"
 
-NewDefinition GameLogic.or_inl
+NewLemma GameLogic.or_inl
+NewDefinition GameLogic.or_def
 
 Introduction "
 # Or Introduction Left
diff --git a/Game/Levels/OrIntro/L02.lean b/Game/Levels/OrIntro/L02.lean
index c4b699d..8c57790 100755
--- a/Game/Levels/OrIntro/L02.lean
+++ b/Game/Levels/OrIntro/L02.lean
@@ -6,7 +6,7 @@ World "OrIntro"
 Level 2
 Title "Right Evidence"
 
-NewDefinition GameLogic.or_inr
+NewLemma GameLogic.or_inr
 
 Introduction "
 # Or Introduction Right
diff --git a/Game/Levels/OrIntro/L03.lean b/Game/Levels/OrIntro/L03.lean
index e15dfc3..22d5fef 100755
--- a/Game/Levels/OrIntro/L03.lean
+++ b/Game/Levels/OrIntro/L03.lean
@@ -6,15 +6,15 @@ World "OrIntro"
 Level 3
 Title "Or Elimination"
 
-NewDefinition GameLogic.or_elim
+NewLemma GameLogic.or_elim
 
 Introduction "
 # Party Games
-Here's the deal. Jaime and Alan both said they're bringing board games and you're sure at least one of them is going to make it. So there's definitely board games at the party!
+Here's the deal. Ilyn and Cyna both said they're bringing board games and you're sure at least one of them is going to make it. So there's definitely board games at the party!
 # Proposition Key:
-- `A` — Alan is coming to the party
 - `B` — There will be boardgames at the party
-- `J` — Jaime is coming to the party
+- `C` — Cyna is coming to the party
+- `I` — Ilyn is coming to the party
 # Or Elimination
 If you can conclude something from `A` and you can conclude the same thing from `B`, then if you know `A ∨ B` it won't matter which of the two happens as you can still guarentee something.
 # You've unlocked `or_elim`
@@ -33,7 +33,7 @@ have r : R := or_elim pvq pr qr
 "
 
 /-- `or_elim h₃ ... ...` -/
-Statement (A B J : Prop)(h₁ : A → B)(h₂ : J → B)(h₃ : A ∨ J) : B := by
+Statement (B C I : Prop)(h₁ : C → B)(h₂ : I → B)(h₃ : C ∨ I) : B := by
   exact or_elim h₃ h₁ h₂
 
 Conclusion "
diff --git a/Game/Levels/OrIntro/L05.lean b/Game/Levels/OrIntro/L05.lean
index 3968711..576cdca 100755
--- a/Game/Levels/OrIntro/L05.lean
+++ b/Game/Levels/OrIntro/L05.lean
@@ -6,6 +6,8 @@ World "OrIntro"
 Level 5
 Title "Carry On Effects"
 
+NewLemma GameLogic.or_comm
+
 Introduction "
 # Carry On Effects
 If the cake arrives, then everybody will rejoice. Either the cake arrives or you get a refund. Therefore, either everybody will rejoice or you get a refund! That's a win-win situation.