major changes

Author: hjvromen

docs/GUIDE.md GUIDE.mddocs/GUIDE.md renamed to GUIDE.md

@@ -45,7 +45,7 @@ section Lewis
 
 variable {indiv : Type*}
 variable (A φ : Prop)
-variable {R : indiv → Prop → Prop}
+variable (R : indiv → Prop → Prop)
 variable {Ind : Prop → indiv → Prop → Prop}
 
 /-!
@@ -184,7 +184,7 @@ This formalizes Lewis's claim that common knowledge is not circular but rather a
 infinite consequence of finite, non-circular conditions.
 -/
 
-lemma lewis_theorem: @RC indiv R φ p → ∀ i, R i p := by
+lemma lewis_theorem: RC R φ p → ∀ i, R i p := by
   intro hp i
   suffices Ind A i p by exact A1 this (C1 i)
   induction hp with