diff --git a/Foundation/Logic/ForcingRelation.lean b/Foundation/Logic/ForcingRelation.lean
index e5dc9eccd..e80ddc26f 100644
--- a/Foundation/Logic/ForcingRelation.lean
+++ b/Foundation/Logic/ForcingRelation.lean
@@ -7,12 +7,11 @@ namespace LO
 
 class ForcingRelation (W : Type*) (F : outParam Type*) where
   Forces : W → F → Prop
-
 infix:45 " ⊩ " => ForcingRelation.Forces
 
+
 class ForcingExists (W : Type*) (α : outParam Type*) where
   Forces : W → α → Prop
-
 infix:45 " ⊩↓ " => ForcingExists.Forces
 
 namespace ForcingRelation
@@ -20,48 +19,62 @@ namespace ForcingRelation
 variable {W : Type*} {F : Type*} [ForcingRelation W F] [LogicalConnective F]
 
 abbrev NotForces (w : W) (φ : F) : Prop := ¬w ⊩ φ
-
 infix:45 " ⊮ " => NotForces
 
 variable (W)
 
 class BasicSemantics where
-  verum (w : W) : w ⊩ ⊤
-  falsum (w : W) : ¬w ⊩ ⊥
-  and (w : W) : w ⊩ φ ⋏ ψ ↔ w ⊩ φ ∧ w ⊩ ψ
-  or (w : W) : w ⊩ φ ⋎ ψ ↔ w ⊩ φ ∨ w ⊩ ψ
+  verum {w : W} : w ⊩ ⊤
+  falsum {w : W} : ¬w ⊩ ⊥
+  and {φ ψ} {w : W} : w ⊩ φ ⋏ ψ ↔ w ⊩ φ ∧ w ⊩ ψ
+  or {φ ψ} {w : W} : w ⊩ φ ⋎ ψ ↔ w ⊩ φ ∨ w ⊩ ψ
 
 class IntKripke (R : outParam (W → W → Prop)) extends BasicSemantics W where
-  not (w : W) : w ⊩ ∼φ ↔ (∀ v, R w v → ¬v ⊩ φ)
-  imply (w : W) : w ⊩ φ ➝ ψ ↔ (∀ v, R w v → v ⊩ φ → v ⊩ ψ)
-  monotone {w : W} : w ⊩ φ → ∀ v, R w v → v ⊩ φ
+  not {φ} {w : W} : w ⊩ ∼φ ↔ (∀ v, R w v → ¬v ⊩ φ)
+  imply {φ ψ} {w : W} : w ⊩ φ ➝ ψ ↔ (∀ v, R w v → v ⊩ φ → v ⊩ ψ)
+  monotone {φ} {w : W} : w ⊩ φ → ∀ v, R w v → v ⊩ φ
 
 variable {W}
 
-attribute [simp, grind]
-  BasicSemantics.verum BasicSemantics.falsum BasicSemantics.and
-  BasicSemantics.or IntKripke.imply IntKripke.not
+attribute [simp, grind .]
+  BasicSemantics.verum
+  BasicSemantics.falsum
 
-variable (W)
+attribute [simp, grind .]
+  BasicSemantics.and
+  BasicSemantics.or
 
-abbrev AllForces (φ : F) : Prop := ∀ w : W, w ⊩ φ
+attribute [simp, grind .]
+  IntKripke.imply
+  IntKripke.not
 
-infix:45 " ∀⊩ " => AllForces
+attribute [grind <=]
+  IntKripke.monotone
+
+variable (W)
 
-abbrev AllForcesSet (s : S) [AdjunctiveSet F S] : Prop := ∀ φ ∈ s, W ∀⊩ φ
+@[grind] def AllForces (φ : F) : Prop := ∀ w : W, w ⊩ φ
+infix:45 " ∀⊩ " => AllForces
 
+@[grind] def AllForcesSet (s : S) [AdjunctiveSet F S] : Prop := ∀ φ ∈ s, W ∀⊩ φ
 infix:45 " ∀⊩* " => AllForcesSet
 
 variable {W}
 
 namespace AllForces
 
-@[simp] lemma verum [BasicSemantics W] : W ∀⊩ ⊤ := fun _ ↦ by simp
-
-@[simp] lemma falsum [BasicSemantics W] [Inhabited W] : ¬W ∀⊩ ⊥ := fun h ↦ by simpa using h default
-
-@[simp] lemma and [BasicSemantics W] : W ∀⊩ φ ⋏ ψ ↔ W ∀⊩ φ ∧ W ∀⊩ ψ := by
-  simp [AllForces]; grind
+@[simp, grind .] lemma verum [BasicSemantics W] : W ∀⊩ ⊤ := fun _ ↦ by simp
+@[simp, grind .] lemma falsum [BasicSemantics W] [Nonempty W] : ¬W ∀⊩ ⊥ := fun h ↦ by simpa using h (Nonempty.some inferInstance)
+
+@[simp, grind =]
+lemma and {φ ψ} [BasicSemantics W] : W ∀⊩ φ ⋏ ψ ↔ W ∀⊩ φ ∧ W ∀⊩ ψ := by
+  constructor;
+  . intro h;
+    constructor <;>
+    . intro w;
+      have := h w;
+      grind;
+  . grind;
 
 end AllForces
 
diff --git a/Foundation/Propositional/Kripke/Basic.lean b/Foundation/Propositional/Kripke/Basic.lean
index e32e71747..88cfab43b 100644
--- a/Foundation/Propositional/Kripke/Basic.lean
+++ b/Foundation/Propositional/Kripke/Basic.lean
@@ -71,75 +71,52 @@ open Formula
 
 namespace Formula.Kripke
 
-def Satisfies (M : Kripke.Model) (w : M.World) : Formula ℕ → Prop
+@[grind]
+def Forces (M : outParam Kripke.Model) (w : M.World) : Formula ℕ → Prop
   | atom a => M w a
   | ⊥      => False
-  | φ ⋏ ψ  => Satisfies M w φ ∧ Satisfies M w ψ
-  | φ ⋎ ψ  => Satisfies M w φ ∨ Satisfies M w ψ
-  | φ ➝ ψ => ∀ {w' : M.World}, (w ≺ w') → (Satisfies M w' φ → Satisfies M w' ψ)
+  | φ ⋏ ψ  => Forces M w φ ∧ Forces M w ψ
+  | φ ⋎ ψ  => Forces M w φ ∨ Forces M w ψ
+  | φ ➝ ψ => ∀ {v : M.World}, (w ≺ v) → (Forces M v φ → Forces M v ψ)
+notation:75 x " ⊩[" M "] " φ:50 => Forces M x φ
 
-namespace Satisfies
+abbrev NotForces (M : outParam Kripke.Model) (w : M.World) (φ : Formula ℕ) : Prop := ¬(w ⊩[M] φ)
+notation:50 x " ⊮[" M "] " φ:50 => NotForces M x φ
 
-instance semantics (M : Kripke.Model) : Semantics M (Formula ℕ) := ⟨fun w ↦ Formula.Kripke.Satisfies M w⟩
+namespace Forces
 
-variable {M : Kripke.Model} {w w' : M.World} {a : ℕ} {φ ψ χ : Formula ℕ}
+variable {M : Kripke.Model} {x y : M.World} {a : ℕ} {φ ψ χ : Formula ℕ}
 
-@[simp] protected lemma iff_models : w ⊧ φ ↔ Formula.Kripke.Satisfies M w φ := iff_of_eq rfl
+@[grind =] lemma def_atom : x ⊩[M] #a ↔ M x a := by tauto;
+@[simp, grind .] lemma def_bot : x ⊮[M] ⊥ := by tauto;
+@[simp, grind .] lemma def_top : x ⊩[M] ⊤ := by tauto;
+@[grind =] lemma def_and : x ⊩[M] φ ⋏ ψ ↔ x ⊩[M] φ ∧ x ⊩[M] ψ := by rfl;
+@[grind =] lemma def_or  : x ⊩[M] φ ⋎ ψ ↔ x ⊩[M] φ ∨ x ⊩[M] ψ := by rfl;
+@[grind =] lemma def_imp : x ⊩[M] φ ➝ ψ ↔ ∀ {v}, x ≺ v → v ⊩[M] φ → v ⊩[M] ψ := by rfl;
+@[grind =] lemma def_neg : x ⊩[M] ∼φ ↔ ∀ {v}, x ≺ v → v ⊮[M] φ := by rfl;
 
-@[simp] lemma atom_def : w ⊧ atom a ↔ M w a := by simp [Satisfies];
-
-@[simp] lemma top_def  : w ⊧ ⊤ ↔ True := by simp [Satisfies];
-
-@[simp] lemma bot_def  : w ⊧ ⊥ ↔ False := by simp [Satisfies];
-
-@[simp] lemma and_def  : w ⊧ φ ⋏ ψ ↔ w ⊧ φ ∧ w ⊧ ψ := by simp [Satisfies];
-
-@[simp] lemma or_def   : w ⊧ φ ⋎ ψ ↔ w ⊧ φ ∨ w ⊧ ψ := by simp [Satisfies];
-
-@[simp] lemma imp_def  : w ⊧ φ ➝ ψ ↔ ∀ {w' : M.World}, (w ≺ w') → (w' ⊧ φ → w' ⊧ ψ) := by simp [Satisfies, imp_iff_not_or];
-
-@[simp] lemma neg_def  : w ⊧ ∼φ ↔ ∀ {w' : M.World}, (w ≺ w') → ¬(w' ⊧ φ) := by simp [Satisfies];
-
-lemma not_of_neg : w ⊧ ∼φ → ¬w ⊧ φ := fun h hC ↦ h (refl w) hC
-
-instance : Semantics.Top M.World where
-  models_verum := by simp [Satisfies];
-
-instance : Semantics.Bot M.World where
-  models_falsum := by simp [Semantics.NotModels, Satisfies];
-
-instance : Semantics.And M.World where
-  models_and := by simp [Satisfies];
-
-instance : Semantics.Or M.World where
-  models_or := by simp [Satisfies];
-
-lemma formula_hereditary
-  (hw : w ≺ w') : w ⊧ φ → w' ⊧ φ := by
+@[grind <=]
+lemma formula_hereditary (Rxy : x ≺ y) : x ⊩[_] φ → y ⊩[_] φ := by
   induction φ with
-  | hatom => apply M.Val.hereditary hw;
-  | himp =>
-    intro hpq v hv;
-    exact hpq $ M.trans hw hv;
-  | hor => simp_all; tauto;
-  | _ => simp_all;
-
-lemma formula_hereditary_not (hw : w ≺ w') : ¬w' ⊧ φ → ¬w ⊧ φ := by
-  contrapose;
-  push_neg;
-  exact formula_hereditary hw;
+  | hatom => apply M.Val.hereditary Rxy;
+  | himp φ ψ ihφ ihψ =>
+    intro h z Ryz hzφ;
+    exact h (M.trans Rxy Ryz) hzφ
+  | _ => grind;
+
+@[grind →] lemma not_of_neg : x ⊩[_] (∼φ) → ¬x ⊩[_] φ := fun h hC ↦ h (refl x) hC
 
-lemma negEquiv : w ⊧ ∼φ ↔ w ⊧ φ ➝ ⊥ := by simp_all [Satisfies];
+-- lemma negEquiv : x ⊩ ∼φ ↔ x ⊩ φ ➝ ⊥ := by simp_all [Forces];
 
 lemma iff_subst_self {F : Frame} {V : Valuation F} {x : F.World} (s) :
   letI U : Kripke.Valuation F := ⟨
-    λ w a => Satisfies ⟨F, V⟩ w ((.atom a)⟦s⟧),
+    λ w a => Forces (M := ⟨F, V⟩) w ((.atom a)⟦s⟧),
     fun {_ _} Rwv {_} => formula_hereditary Rwv
   ⟩;
-  Satisfies ⟨F, U⟩ x φ ↔ Satisfies ⟨F, V⟩ x (φ⟦s⟧) := by
+  x ⊩[⟨F, U⟩] φ ↔ x ⊩[⟨F, V⟩] (φ⟦s⟧) := by
   induction φ generalizing x with
-  | hatom a => simp [Satisfies];
-  | hfalsum => simp [Satisfies];
+  | hatom a => simp [Forces];
+  | hfalsum => simp [Forces];
   | himp φ ψ ihφ ihψ =>
     constructor;
     . intro hφψ y Rxy hφs;
@@ -157,7 +134,7 @@ lemma iff_subst_self {F : Frame} {V : Valuation F} {x : F.World} (s) :
       . apply ihφ.mp hφ;
       . apply ihψ.mp hψ;
     . rintro ⟨hφ, hψ⟩;
-      apply Satisfies.and_def.mpr;
+      apply def_and.mpr;
       constructor;
       . apply ihφ.mpr hφ;
       . apply ihψ.mpr hψ;
@@ -170,51 +147,30 @@ lemma iff_subst_self {F : Frame} {V : Valuation F} {x : F.World} (s) :
       . left; apply ihφ.mpr hφ;
       . right; apply ihψ.mpr hψ;
 
-end Satisfies
+end Forces
 
 
-open Satisfies
-
-def ValidOnModel (M : Kripke.Model) (φ : Formula ℕ) := ∀ w : M.World, w ⊧ φ
+open Forces
 
 namespace ValidOnModel
 
-instance semantics : Semantics Model (Formula ℕ) := ⟨fun M ↦ Formula.Kripke.ValidOnModel M⟩
+instance : Semantics (Kripke.Model) (Formula ℕ) := ⟨fun M φ => ∀ x : M.World, x ⊩[M] φ⟩
 
 variable {M : Model} {φ ψ χ : Formula ℕ}
 
-@[simp] protected lemma iff_models : M ⊧ φ ↔ Formula.Kripke.ValidOnModel M φ := iff_of_eq rfl
-
-
-protected lemma verum : M ⊧ ⊤ := by simp [ValidOnModel];
-
-instance : Semantics.Top (Model) := ⟨λ _ => ValidOnModel.verum⟩
-
+@[simp, grind =] lemma iff_models : M ⊧ φ ↔ ∀ x : M.World, x ⊩[M] φ := iff_of_eq rfl
+@[simp, grind =] lemma iff_not_models : M ⊭ φ ↔ ∃ x : M.World, x ⊮[M] φ := by simp [Semantics.NotModels, Semantics.Models];
 
-protected lemma bot : ¬M ⊧ ⊥ := by simp [ValidOnModel];
-
-instance : Semantics.Bot (Model) := ⟨λ _ => ValidOnModel.bot⟩
-
-
-lemma iff_not_exists_world {M : Kripke.Model} : (¬M ⊧ φ) ↔ (∃ x : M.World, ¬x ⊧ φ) := by
-  apply not_iff_not.mp;
-  push_neg;
-  tauto;
+instance : Semantics.Top Model := ⟨by simp⟩
+instance : Semantics.Bot Model := ⟨by simp⟩
 
-alias ⟨exists_world_of_not, not_of_exists_world⟩ := iff_not_exists_world
+alias ⟨exists_world_of_not, not_of_exists_world⟩ := iff_not_models
 
-protected lemma andElim₁ : M ⊧ φ ⋏ ψ ➝ φ := by simp_all [ValidOnModel, Satisfies];
-
-protected lemma andElim₂ : M ⊧ φ ⋏ ψ ➝ ψ := by simp_all [ValidOnModel, Satisfies];
-
-protected lemma andInst₃ : M ⊧ φ ➝ ψ ➝ φ ⋏ ψ := by
-  intro x y _ hp z Ryz hq;
-  replace hp : Satisfies M z φ := formula_hereditary Ryz hp;
-  exact ⟨hp, hq⟩;
-
-protected lemma orInst₁ : M ⊧ φ ➝ φ ⋎ ψ := by simp_all [ValidOnModel, Satisfies];
-
-protected lemma orInst₂ : M ⊧ ψ ➝ φ ⋎ ψ := by simp_all [ValidOnModel, Satisfies];
+protected lemma andElim₁ : M ⊧ φ ⋏ ψ ➝ φ := by grind;
+protected lemma andElim₂ : M ⊧ φ ⋏ ψ ➝ ψ := by grind;
+protected lemma andInst₃ : M ⊧ φ ➝ ψ ➝ φ ⋏ ψ := by grind;
+protected lemma orInst₁ : M ⊧ φ ➝ φ ⋎ ψ := by grind;
+protected lemma orInst₂ : M ⊧ ψ ➝ φ ⋎ ψ := by grind;
 
 protected lemma orElim : M ⊧ (φ ➝ χ) ➝ (ψ ➝ χ) ➝ (φ ⋎ ψ ➝ χ) := by
   intro w₁ w₂ _ hpr w₃ hw₂₃ hqr w₄ hw₃₄ hpq;
@@ -222,9 +178,7 @@ protected lemma orElim : M ⊧ (φ ➝ χ) ➝ (ψ ➝ χ) ➝ (φ ⋎ ψ ➝ χ
   | inl hp => exact hpr (M.trans hw₂₃ hw₃₄) hp;
   | inr hq => exact hqr hw₃₄ hq;
 
-protected lemma implyK : M ⊧ φ ➝ ψ ➝ φ := by
-  intro x y _ hp z Ryz _;
-  exact formula_hereditary Ryz hp;
+protected lemma implyK : M ⊧ φ ➝ ψ ➝ φ := by grind;
 
 protected lemma implyS : M ⊧ (φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ := by
   intro x y _ hpqr z Ryz hpq w Rzw hp;
@@ -236,59 +190,38 @@ protected lemma mdp (hpq : M ⊧ φ ➝ ψ) (hp : M ⊧ φ) : M ⊧ ψ := by
   intro w;
   exact hpq w M.refl $ hp w;
 
-protected lemma efq : M ⊧ Axioms.EFQ φ := by simp [ValidOnModel, Satisfies];
+protected lemma efq : M ⊧ Axioms.EFQ φ := by grind;
 
 end ValidOnModel
 
 
-def ValidOnFrame (F : Frame) (φ : Formula ℕ) := ∀ V, (⟨F, V⟩ : Kripke.Model) ⊧ φ
-
 
 namespace ValidOnFrame
 
-instance semantics : Semantics Frame (Formula ℕ) := ⟨fun F ↦ Formula.Kripke.ValidOnFrame F⟩
+instance : Semantics Frame (Formula ℕ) := ⟨fun F φ => ∀ V, (⟨F, V⟩ : Kripke.Model) ⊧ φ⟩
 
 variable {F : Frame} {φ ψ χ : Formula ℕ}
 
-@[simp] protected lemma models_iff : F ⊧ φ ↔ ValidOnFrame F φ := iff_of_eq rfl
+@[simp, grind .] lemma iff_valid : F ⊧ φ ↔ ∀ V, (⟨F, V⟩ : Kripke.Model) ⊧ φ := by rfl
+@[simp, grind .] lemma iff_not_valid : F ⊭ φ ↔ ∃ V, (⟨F, V⟩ : Kripke.Model) ⊭ φ := by simp [Semantics.NotModels, Semantics.Models];
+alias ⟨exists_valuation_of_not, not_of_exists_valuation⟩ := iff_not_valid
+
+lemma iff_not_exists_valuation_world : (F ⊭ φ) ↔ (∃ V x, x ⊮[⟨F, V⟩] φ) := by grind;
+alias ⟨exists_valuation_world_of_not, not_of_exists_valuation_world⟩ := iff_not_exists_valuation_world
 
 protected lemma top : F ⊧ ⊤ := by tauto;
 instance : Semantics.Top (Frame) := ⟨λ _ => ValidOnFrame.top⟩
 
-protected lemma bot : ¬F ⊧ ⊥ := by
-  simp [ValidOnFrame.models_iff, ValidOnFrame];
-  exact ⟨(λ _ _ => True), by tauto⟩;
+protected lemma bot : F ⊭ ⊥ := by
+  apply not_of_exists_valuation_world;
+  use ⟨λ _ _ => True, by tauto⟩, F.world_nonempty.some;
+  grind;
 instance : Semantics.Bot (Frame) := ⟨λ _ => ValidOnFrame.bot⟩
 
-
-lemma iff_not_exists_valuation : (¬F ⊧ φ) ↔ (∃ V : Kripke.Valuation F, ¬(⟨F, V⟩ : Kripke.Model) ⊧ φ) := by
-  simp [ValidOnFrame];
-
-alias ⟨exists_valuation_of_not, not_of_exists_valuation⟩ := iff_not_exists_valuation
-
-
-lemma iff_not_exists_valuation_world : (¬F ⊧ φ) ↔ (∃ V : Kripke.Valuation F, ∃ x : (⟨F, V⟩ : Kripke.Model).World, ¬Satisfies _ x φ) := by
-  simp [ValidOnFrame, ValidOnModel, Semantics.Models];
-
-alias ⟨exists_valuation_world_of_not, not_of_exists_valuation_world⟩ := iff_not_exists_valuation_world
-
-
-lemma iff_not_exists_model_world :  (¬F ⊧ φ) ↔ (∃ M : Kripke.Model, ∃ x : M.World, M.toFrame = F ∧ ¬(x ⊧ φ)) := by
-  constructor;
-  . intro h;
-    obtain ⟨V, x, h⟩ := iff_not_exists_valuation_world.mp h;
-    use ⟨F, V⟩, x;
-    tauto;
-  . rintro ⟨M, x, rfl, h⟩;
-    exact iff_not_exists_valuation_world.mpr ⟨M.Val, x, h⟩;
-
-alias ⟨exists_model_world_of_not, not_of_exists_model_world⟩ := iff_not_exists_model_world
-
-
 protected lemma subst (h : F ⊧ φ) : F ⊧ φ⟦s⟧ := by
   by_contra hC;
   obtain ⟨V, ⟨x, hx⟩⟩ := exists_valuation_world_of_not hC;
-  apply Satisfies.iff_subst_self s |>.not.mpr hx;
+  apply Forces.iff_subst_self s |>.not.mpr hx;
   apply h;
 
 protected lemma andElim₁ : F ⊧ φ ⋏ ψ ➝ φ := fun _ => ValidOnModel.andElim₁
@@ -323,28 +256,23 @@ section
 
 variable {C : Kripke.FrameClass} {φ ψ χ : Formula ℕ}
 
-lemma iff_not_validOnFrameClass_exists_frame : (¬C ⊧ φ) ↔ (∃ F ∈ C, ¬F ⊧ φ) := by
+lemma iff_not_validOnFrameClass_exists_frame : C ⊭ φ ↔ (∃ F ∈ C, F ⊭ φ) := by
   apply not_iff_not.mp;
   push_neg;
   tauto;
 alias ⟨exists_frame_of_not_validOnFrameClass, not_validOnFrameClass_of_exists_frame⟩ := iff_not_validOnFrameClass_exists_frame
 
-lemma iff_not_validOnFrameClass_exists_model : (¬C ⊧ φ) ↔ (∃ M : Kripke.Model, M.toFrame ∈ C ∧ ¬M ⊧ φ) := by
+lemma iff_not_validOnFrameClass_exists_model : C ⊭ φ ↔ (∃ M : Kripke.Model, M.toFrame ∈ C ∧ ¬M ⊧ φ) := by
   apply not_iff_not.mp;
   push_neg;
   tauto;
 alias ⟨exists_model_of_not_validOnFrameClass, not_validOnFrameClass_of_exists_model⟩ := iff_not_validOnFrameClass_exists_model
 
-lemma iff_not_validOnFrameClass_exists_model_world : (¬C ⊧ φ) ↔ (∃ M : Kripke.Model, ∃ x : M.World, M.toFrame ∈ C ∧ ¬(x ⊧ φ)) := by
-  apply not_iff_not.mp;
-  push_neg;
-  tauto;
-alias ⟨exists_model_world_of_not_validOnFrameClass, not_validOnFrameClass_of_exists_model_world⟩ := iff_not_validOnFrameClass_exists_model_world
-
 end
 
 
 
+/-
 section
 
 open Formula (atom)
@@ -366,14 +294,14 @@ lemma Validates.inter_of (h₁ : C₁.Validates Γ₁) (h₂ : C₂.Validates Γ
 lemma ValidatesFormula.inter_of (h₁ : C₁.ValidatesFormula φ₁) (h₂ : C₂.ValidatesFormula φ₂) : (C₁ ∩ C₂).Validates {φ₁, φ₂}
   := Validates.inter_of h₁ h₂
 
-
 protected abbrev all : FrameClass := Set.univ
 
 @[simp]
 lemma all.IsNonempty : FrameClass.all.Nonempty := by use whitepoint; tauto;
 
 lemma all.validates_AxiomEFQ : FrameClass.all.ValidatesFormula (Axioms.EFQ (.atom 0)) := by
-  suffices ∀ (F : Frame), Formula.Kripke.ValidOnFrame F (Axioms.EFQ (.atom 0)) by simpa [Validates];
+
+  suffices ∀ F : Frame, F ⊨ (Axioms.EFQ (.atom 0)) by simpa [Validates];
   intro F;
   exact Formula.Kripke.ValidOnFrame.efq;
 
@@ -387,14 +315,14 @@ protected abbrev finite_all : FrameClass := { F | F.IsFinite }
 lemma finite_all.nonempty : FrameClass.finite_all.Nonempty := by use whitepoint; tauto;
 
 lemma finite_all.validates_AxiomEFQ : FrameClass.finite_all.ValidatesFormula (Axioms.EFQ (.atom 0)) := by
-  suffices ∀ (F : Frame), F.IsFinite → Formula.Kripke.ValidOnFrame F (Axioms.EFQ (.atom 0)) by simpa [Validates];
+  suffices ∀ (F : Frame), F.IsFinite → F ⊨ (Axioms.EFQ (.atom 0)) by simpa [Validates];
   intro F _;
   exact Formula.Kripke.ValidOnFrame.efq;
 
 end FrameClass
 
 end
-
+-/
 
 section