diff --git a/Pdl/LocalTableau.lean b/Pdl/LocalTableau.lean
index 0204f0d..f29ae52 100644
--- a/Pdl/LocalTableau.lean
+++ b/Pdl/LocalTableau.lean
@@ -5,7 +5,7 @@ import Pdl.MultisetOrder
 
 open HasLength
 
--- TABLEAU NODES
+/-! ## Tableau Nodes -/
 
 -- A tableau node has two lists of formulas and one or no negated loaded formula.
 -- TODO: rename `TNode` to `Sequent`
@@ -49,6 +49,8 @@ theorem setEqTo_isLoaded_iff {X Y : TNode} (h : X.setEqTo Y) : X.isLoaded = Y.is
   all_goals
     exfalso; rcases h with ⟨_,_,impossible⟩ ; exact (Bool.eq_not_self _).mp impossible
 
+/-! ## Semantics of a TNode -/
+
 instance modelCanSemImplyTNode : vDash (KripkeModel W × W) TNode :=
   vDash.mk (λ ⟨M,w⟩ ⟨L, R, o⟩ => ∀ f ∈ L ∪ R ∪ (o.map (Sum.elim negUnload negUnload)).toList, evaluate M w f)
 
@@ -69,6 +71,24 @@ theorem tautImp_iff_TNodeUnsat {φ ψ} {X : TNode} :
   subst defX
   simp [satisfiable,evaluate,modelCanSemImplyTNode,formCanSemImplyForm,semImpliesLists] at *
 
+/-! ## Different kinds of formulas as elements of TNode -/
+
+@[simp]
+instance : Membership Formula TNode := ⟨fun φ X => φ ∈ X.L ∨ φ ∈ X.R⟩
+
+def NegLoadFormula_in_TNode (nlf : NegLoadFormula) (X : TNode) : Prop :=
+  X.O = some (Sum.inl nlf) ∨ X.O = some (Sum.inr nlf)
+
+@[simp]
+instance : Membership NegLoadFormula TNode := ⟨NegLoadFormula_in_TNode⟩
+
+def AnyNegFormula_in_TNode : (anf : AnyNegFormula) → (X : TNode) → Prop
+| ⟨.normal φ⟩, X => (~φ) ∈ X
+| ⟨.loaded χ⟩, X => NegLoadFormula_in_TNode (~'χ) X -- FIXME: ∈ not working here
+
+@[simp]
+instance : Membership AnyNegFormula TNode := ⟨AnyNegFormula_in_TNode⟩
+
 /-! ## Local Tableaux -/
 
 /-- A set is closed iff it contains `⊥` or contains a formula and its negation. -/
diff --git a/Pdl/Modelgraphs.lean b/Pdl/Modelgraphs.lean
index 14bc308..e620591 100644
--- a/Pdl/Modelgraphs.lean
+++ b/Pdl/Modelgraphs.lean
@@ -56,7 +56,7 @@ theorem loadClaimHelper {Worlds : Finset (Finset Formula)}
     {X Y : { x // x ∈ Worlds }}
     {δ : List Program}
     {φ : Formula}
-    {l: List { x // x ∈ Worlds }}
+    {l : List { x // x ∈ Worlds }}
     (length_def: l.length + 1 = δ.length)
     (δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ X.val)
     (lchain : List.Chain' (pairRel MG.1) (List.zip ((?'⊤) :: δ) (X :: l ++ [Y])))
diff --git a/Pdl/Semantics.lean b/Pdl/Semantics.lean
index 70f2503..3e44fc9 100644
--- a/Pdl/Semantics.lean
+++ b/Pdl/Semantics.lean
@@ -108,6 +108,10 @@ instance modelCanSemImplyForm {W : Type} : vDash (KripkeModel W × W) Formula :=
 instance modelCanSemImplySet {W : Type} : vDash (KripkeModel W × W) (List Formula) := vDash.mk (λ ⟨M,w⟩ fs => ∀ f ∈ fs, @evaluate W M w f)
 @[simp]
 instance modelCanSemImplyList {W : Type} : vDash (KripkeModel W × W) (List Formula) := vDash.mk (λ ⟨M,w⟩ fs => ∀ f ∈ fs, @evaluate W M w f)
+instance modelCanSemImplyAnyNegFormula {W : Type} : vDash (KripkeModel W × W) AnyNegFormula :=
+  vDash.mk (λ ⟨M,w⟩ af => match af with
+   | ⟨.normal f⟩ => evaluate M w f
+   | ⟨.loaded f⟩ => evaluate M w (unload f) )
 instance setCanSemImplySet : vDash (List Formula) (List Formula) := vDash.mk semImpliesLists
 instance setCanSemImplyForm : vDash (List Formula) Formula:= vDash.mk fun X ψ => semImpliesLists X [ψ]
 instance formCanSemImplySet : vDash Formula (List Formula) := vDash.mk fun φ X => semImpliesLists [φ] X
diff --git a/Pdl/Soundness.lean b/Pdl/Soundness.lean
index eda6d95..f224a72 100644
--- a/Pdl/Soundness.lean
+++ b/Pdl/Soundness.lean
@@ -14,7 +14,7 @@ open HasSat
 /-- The PDL rules are sound. -/
 theorem pdlRuleSat (r : PdlRule X Y) (satX : satisfiable X) : satisfiable Y := by
   rcases satX with ⟨W, M, w, w_⟩
-  -- 8 cases, quite some duplication here unfortunately.
+  -- 6 cases, quite some duplication here unfortunately.
   cases r
   -- the loading rules are easy, because loading never changes semantics
   case loadL =>
@@ -22,141 +22,97 @@ theorem pdlRuleSat (r : PdlRule X Y) (satX : satisfiable X) : satisfiable Y := b
     simp_all [modelCanSemImplyTNode]
     intro φ φ_in
     rcases φ_in with ((in_L | in_R) | φ_def)
-    all_goals
-      apply w_
-      subst_eqs
-      try tauto
-    · left
-      exact List.mem_of_mem_erase in_L
-    · left
-      simp [toNegLoad, unload]
-      sorry
+    all_goals (apply w_;  subst_eqs; try tauto)
+    left; exact List.mem_of_mem_erase in_L
   case loadR =>
     use W, M, w
     simp_all [modelCanSemImplyTNode]
-    sorry
+    intro φ φ_in
+    rcases φ_in with ((in_L | in_R) | φ_def)
+    all_goals (apply w_;  subst_eqs; try tauto)
+    right; exact List.mem_of_mem_erase in_R
   case freeL =>
     use W, M, w
     simp_all [modelCanSemImplyTNode]
-    sorry
+    intro φ φ_in
+    rcases φ_in with (φ_def | (in_L | in_R))
+    all_goals (apply w_;  subst_eqs; try tauto)
   case freeR =>
     use W, M, w
     simp_all [modelCanSemImplyTNode]
-    sorry
-  case atmL L R a χ X_def x_basic =>
-    subst X_def
-    use W, M -- but not the same world!
-    have := w_ (negUnload (~'⌊·a⌋χ))
-    simp at this
-    rcases this with ⟨v, w_a_b, v_⟩
-    use v
     intro φ φ_in
-    simp at φ_in
-    rcases φ_in with ((in_L | in_R) | φ_def)
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-    · subst φ_def
-      simp only [evaluate]
-      assumption
-  case atmR L R a χ X_def x_basic =>
+    rcases φ_in with (φ_def | (in_L | in_R))
+    all_goals (apply w_;  subst_eqs; try tauto)
+  case modL L R a χ X_def x_basic =>
     subst X_def
     use W, M -- but not the same world!
     have := w_ (negUnload (~'⌊·a⌋χ))
-    simp at this
-    rcases this with ⟨v, w_a_b, v_⟩
-    use v
-    intro φ φ_in
-    simp at φ_in
-    rcases φ_in with ((in_L | in_R) | φ_def)
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-    · subst φ_def
-      simp only [evaluate]
-      assumption
-  case atmL' L R a φ X_def x_basic =>
-    subst X_def
-    use W, M -- but not the same world!
-    have := w_ (negUnload (~'⌊·a⌋φ))
-    simp at this
-    rcases this with ⟨v, w_a_b, v_⟩
-    use v
-    intro φ φ_in
-    simp at φ_in
-    rcases φ_in with (φ_def | (in_L | in_R))
-    · subst φ_def
-      simp only [evaluate]
-      assumption
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-  case atmR' L R a φ X_def x_basic =>
+    cases χ
+    · simp [unload] at *
+      rcases this with ⟨v, w_a_b, v_⟩
+      use v
+      intro φ φ_in
+      simp at φ_in
+      rcases φ_in with ( φ_def | (in_L | in_R))
+      · subst φ_def
+        simp only [evaluate]
+        assumption
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+    · simp [unload] at *
+      rcases this with ⟨v, w_a_b, v_⟩
+      use v
+      intro φ φ_in
+      simp at φ_in
+      rcases φ_in with ((in_L | in_R) | φ_def)
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+      · subst φ_def
+        simp only [evaluate]
+        assumption
+  case modR L R a χ X_def x_basic =>
     subst X_def
     use W, M -- but not the same world!
-    have := w_ (negUnload (~'⌊·a⌋φ))
-    simp at this
-    rcases this with ⟨v, w_a_b, v_⟩
-    use v
-    intro φ φ_in
-    simp at φ_in
-    rcases φ_in with (in_L | (φ_def | in_R))
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-    · subst φ_def
-      simp only [evaluate]
-      assumption
-    · have := w_ (⌈·a⌉φ) (by simp; tauto)
-      simp at this;
-      exact this _ w_a_b
-
-/-- ## Tools for saying that different kinds of formulas are in a TNode -/
-
-@[simp]
-instance : Membership Formula TNode :=
-  ⟨fun φ X => φ ∈ X.L ∨ φ ∈ X.R⟩
-
-def NegLoadFormula_in_TNode (nlf : NegLoadFormula) (X : TNode) : Prop :=
-  X.O = some (Sum.inl nlf) ∨ X.O = some (Sum.inr nlf)
-
-@[simp]
-instance NegLoadFormula.HasMem_TNode : Membership NegLoadFormula TNode := ⟨NegLoadFormula_in_TNode⟩
-
-def AnyFormula := Sum Formula LoadFormula
-
-inductive AnyNegFormula
-| neg : AnyFormula → AnyNegFormula
-
-local notation "~''" φ:arg => AnyNegFormula.neg φ
-
-instance modelCanSemImplyAnyNegFormula {W : Type} : vDash (KripkeModel W × W) AnyNegFormula :=
-  vDash.mk (λ ⟨M,w⟩ af => match af with
-   | ⟨Sum.inl f⟩ => evaluate M w f
-   | ⟨Sum.inr f⟩ => evaluate M w (unload f)
-   )
-
-def anyNegLoad : Program → AnyFormula → NegLoadFormula
-| α, Sum.inl φ => ~'⌊α⌋φ
-| α, Sum.inr χ => ~'⌊α⌋χ
-
-local notation "~'⌊" α "⌋" χ => anyNegLoad α χ
-
-def AnyNegFormula_in_TNode := fun (anf : AnyNegFormula) (X : TNode) => match anf with
-| ⟨Sum.inl φ⟩ => (~φ) ∈ X
-| ⟨Sum.inr χ⟩ => NegLoadFormula_in_TNode (~'χ) X -- FIXME: ∈ not working here
-
-@[simp]
-instance : Membership AnyNegFormula TNode := ⟨AnyNegFormula_in_TNode⟩
+    have := w_ (negUnload (~'⌊·a⌋χ))
+    cases χ
+    · simp [unload] at *
+      rcases this with ⟨v, w_a_b, v_⟩
+      use v
+      intro φ φ_in
+      simp at φ_in
+      rcases φ_in with (in_L | (φ_def | in_R))
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+      · subst φ_def
+        simp only [evaluate]
+        assumption
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+    · simp [unload] at *
+      rcases this with ⟨v, w_a_b, v_⟩
+      use v
+      intro φ φ_in
+      simp at φ_in
+      rcases φ_in with ((in_L | in_R) | φ_def)
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+      · have := w_ (⌈·a⌉φ) (by simp; tauto)
+        simp at this;
+        exact this _ w_a_b
+      · subst φ_def
+        simp only [evaluate]
+        assumption
 
 /-- ## Navigating through tableaux with PathIn -/
 
@@ -315,12 +271,9 @@ match t with
 def PathIn.isCritical (t : PathIn tab) : Prop :=
 match t with
   | .nil => False
-  | .pdl r _ => match r with
-     | .atmL _ _ => True
-     | .atmR _ _ => True
-     | .atmL' _ _ => True
-     | .atmR' _ _ => True
-     | _ => False
+  | .pdl (.modL _ _) _ => True
+  | .pdl (.modR _ _) _ => True
+  | .pdl _ tail => tail.isCritical
   | .loc _ tail => tail.isCritical
 
 /-- Prefix of a path, taking only the first `k` steps. -/
@@ -635,9 +588,21 @@ theorem tableauThenNotSat (tab : ClosedTableau .nil Root) (t : PathIn tab) :
       apply eProp2.c t _ t_is_free t_s
     case pdl Y r ctY =>
       simp [nodeAt]
-      -- use soundness of pdl rules here?!
-      sorry
-
+      intro hyp
+      have := pdlRuleSat r hyp -- using soundness of pdl rules here!
+      absurd this
+      -- As in `loc` case, it now remains to define a path leading to `Y`.
+      let t_to_s : PathIn _ := (@PathIn.pdl _ _ _ ctY r .nil)
+      let s : PathIn tab := t.append (t_def ▸ t_to_s)
+      have t_s : t ◃ s := by
+        unfold_let s
+        sorry
+      have : Y = nodeAt s := by
+        unfold_let s
+        sorry
+      rw [this]
+      apply IH
+      apply eProp2.c t _ t_is_free t_s
 
   case inr not_free =>
     simp [TNode.isFree] at not_free
diff --git a/Pdl/Syntax.lean b/Pdl/Syntax.lean
index e08448d..f293773 100644
--- a/Pdl/Syntax.lean
+++ b/Pdl/Syntax.lean
@@ -77,59 +77,89 @@ theorem boxes_append : Formula.boxes (as ++ bs) P = Formula.boxes as (Formula.bo
   · simp at *
     assumption
 
--- LOADED FORMULAS
+/-! ## Loaded Formulas -/
 
 -- Loaded formulas consist of a negation, a sequence of loading boxes and then a normal formula.
 -- For loading boxes we write ⌊α⌋ instead of ⌈α⌉.
 
-inductive LoadFormula : Type -- χ
-  | load : Program → Formula → LoadFormula -- ⌊α⌋φ
-  | box : Program → LoadFormula → LoadFormula -- ⌊α⌋χ
+mutual
+inductive AnyFormula : Type
+  | normal : Formula → AnyFormula -- φ
+  | loaded : LoadFormula → AnyFormula -- χ
+  deriving Repr, DecidableEq
+
+inductive LoadFormula : Type
+  | box : Program → AnyFormula → LoadFormula -- ⌊α⌋χ
   deriving Repr, DecidableEq
+end
+
+instance : Coe Formula AnyFormula := ⟨AnyFormula.normal⟩
+instance : Coe LoadFormula AnyFormula := ⟨AnyFormula.loaded⟩
+
+inductive AnyNegFormula
+| neg : AnyFormula → AnyNegFormula
 
 @[simp]
 def loadMulti : List Program → Program → Formula → LoadFormula
-| bs, α, φ => List.foldl (flip LoadFormula.box) (LoadFormula.load α φ) bs
+| bs, α, φ => List.foldl (fun f β => LoadFormula.box β f) (LoadFormula.box α φ) bs
 
 @[simp]
 def LoadFormula.boxes : List Program → LoadFormula → LoadFormula
 | [], χ => χ
-| (b::bs), χ => (χ.boxes bs).box b
+| (b::bs), χ => LoadFormula.box b (LoadFormula.boxes bs χ)
 
 @[simp]
 def unload : LoadFormula → Formula
-| LoadFormula.load α φ => ⌈α⌉φ
-| LoadFormula.box α χ => ⌈α⌉(unload χ)
+| LoadFormula.box α (.normal φ) => ⌈α⌉φ
+| LoadFormula.box α (.loaded χ) => ⌈α⌉(unload χ)
 
 inductive NegLoadFormula : Type -- ¬χ
   | neg : LoadFormula → NegLoadFormula
   deriving Repr, DecidableEq
 
-@[simp]
-def negUnload : NegLoadFormula → Formula
-| NegLoadFormula.neg χ => ~(unload χ)
+-- FIXME: find some nice short notation for this and get Lean to use it?
+-- notation "n:" φ:arg => AnyFormula.normal φ
+-- notation "l:" χ:arg => AnyFormula.normal χ
 
-notation "⌊" α "⌋" φ => LoadFormula.load α φ
 notation "⌊" α "⌋" χ => LoadFormula.box α χ
 notation "⌊⌊" αs "⌋⌋" χ => LoadFormula.boxes αs χ
 notation "~'" χ => NegLoadFormula.neg χ
+notation "~''" φ:arg => AnyNegFormula.neg φ
 
-example : NegLoadFormula := ~'(⌊((·1) ;' (·2))⌋⊤)
-example : NegLoadFormula := ~'(⌊⌊[·1, ·2]⌋⌋⌊·1⌋ ⊤)
+@[simp]
+def negUnload : NegLoadFormula → Formula
+| NegLoadFormula.neg χ => ~(unload χ)
 
-theorem loadBoxes_last : (~'⌊a⌋LoadFormula.boxes (as ++ [c]) P) = (~'⌊a⌋LoadFormula.boxes as (⌊c⌋P)) :=
+example : NegLoadFormula := ~'(⌊((·1) ;' (·2))⌋(⊤ : Formula))
+example : NegLoadFormula := ~'(⌊⌊[·1, ·2]⌋⌋⌊·1⌋(⊤ : Formula))
+
+theorem loadBoxes_append : LoadFormula.boxes (as ++ bs) P = LoadFormula.boxes as (LoadFormula.boxes bs P) :=
   by
   induction as
   · simp
   · simp at *
     assumption
 
-theorem loadBoxes_append : LoadFormula.boxes (as ++ bs) P = LoadFormula.boxes as (LoadFormula.boxes bs P) :=
+theorem loadBoxes_last : (~'⌊a⌋LoadFormula.boxes (as ++ [c]) P) = (~'⌊a⌋LoadFormula.boxes as (⌊c⌋P)) :=
   by
   induction as
   · simp
-  · simp at *
-    assumption
+  case cons IH =>
+    simp [loadBoxes_append] at *
+
+@[simp]
+theorem unload_boxes : unload (⌊⌊δ⌋⌋φ) = ⌈⌈δ⌉⌉(unload φ) := by
+  induction δ
+  · simp
+  · simp_all only [LoadFormula.boxes, unload, Formula.boxes]
+
+@[simp]
+theorem unload_neg_loaded : unload (~'⌊α⌋(.loaded χ)).1 = ⌈α⌉(unload χ) := by
+  simp [unload]
+
+@[simp]
+theorem unload_neg_normal : unload (~'⌊α⌋(.normal φ)).1 = ⌈α⌉φ := by
+  simp [unload]
 
 /-! ## Fischer-Ladner Closure -/
 
diff --git a/Pdl/Tableau.lean b/Pdl/Tableau.lean
index c8ea3f2..6ea12c2 100644
--- a/Pdl/Tableau.lean
+++ b/Pdl/Tableau.lean
@@ -34,13 +34,6 @@ def boxesOf : Formula → List Program × Formula
 | (Formula.box prog nextf) => let (rest,endf) := boxesOf nextf; ⟨prog::rest, endf⟩
 | f => ([], f)
 
--- From ~⌈α⌉φ to ~'⌊α⌋χ with maximal loading
-def toNegLoad (α : Program) (φ : Formula) : NegLoadFormula :=
-  let (bs, f) := boxesOf φ
-  match (bs.reverse, f) with -- reverse so we get bs.last for LoadFormula.load.
-    | ([], f) => ~'⌊α⌋f
-    | (b::bs, f) => ~'⌊α⌋(List.foldl (flip LoadFormula.box) (LoadFormula.load b f) bs)
-
 /-- A history is a list of TNodes.
 This only tracks "big" steps, hoping we do not need steps within a local tableau.
 The head of the first list is the newest TNode. -/
@@ -63,24 +56,24 @@ theorem LoadedPathRepeat_isLoaded (lpr : LoadedPathRepeat Hist X) : X.isLoaded :
 /-- A rule to go from Γ to Δ. Note the four variants of the modal rule. -/
 inductive PdlRule : (Γ : TNode) → (Δ : TNode) → Type
   -- The (L+) rule:
-  | loadL : (~⌈α⌉φ) ∈ L → PdlRule (L, R, none)
-                                  (L.erase (~⌈α⌉φ), R, some (Sum.inl (toNegLoad α φ)))
-  | loadR : (~⌈α⌉φ) ∈ R → PdlRule (L, R, none)
-                                  (L, R.erase (~⌈α⌉φ), some (Sum.inr (toNegLoad α φ)))
+  | loadL : (~⌈⌈δ⌉⌉⌈α⌉φ) ∈ L → PdlRule (L, R, none)
+                                       (L.erase (~⌈⌈δ⌉⌉φ), R, some (Sum.inl (~'(⌊⌊δ⌋⌋⌊α⌋φ))))
+  | loadR : (~⌈⌈δ⌉⌉⌈α⌉φ) ∈ R → PdlRule (L, R, none)
+                                       (L, R.erase (~⌈⌈δ⌉⌉φ), some (Sum.inr (~'(⌊⌊δ⌋⌋⌊α⌋φ))))
   -- The (L-) rule:
-  | freeL : PdlRule (L, R, some (Sum.inl (toNegLoad α φ)))
-                    (L.insert (~⌈α⌉φ), R, none)
-  | freeR : PdlRule (L, R, some (Sum.inr (toNegLoad α φ)))
-                    (L, R.insert (~⌈α⌉φ), none)
+  | freeL : PdlRule (L, R, some (Sum.inl (~'(⌊⌊δ⌋⌋⌊α⌋(φ : Formula)))))
+                    (L.insert (~⌈⌈δ⌉⌉⌈α⌉φ), R, none)
+  | freeR : PdlRule (L, R, some (Sum.inr (~'(⌊⌊δ⌋⌋⌊α⌋(φ : Formula)))))
+                    (L, R.insert (~⌈⌈δ⌉⌉⌈α⌉φ), none)
   -- The (M) rule:
-  | atmL   {A X χ} : X = ⟨L, R, some (Sum.inl (~'⌊·A⌋(χ : LoadFormula)))⟩ → isBasic X → PdlRule X
-                         ⟨projection A L, projection A R, some (Sum.inl (~'χ))⟩
-  | atmR   {A X χ} : X = ⟨L, R, some (Sum.inr (~'⌊·A⌋(χ : LoadFormula)))⟩ → isBasic X → PdlRule X
-                         ⟨projection A L, projection A R, some (Sum.inr (~'χ))⟩
-  | atmL'  {A X φ} : X = ⟨L, R, some (Sum.inl (~'⌊·A⌋(φ : Formula)))⟩ → isBasic X → PdlRule X
-                         ⟨(~φ) :: projection A L, projection A R, none⟩
-  | atmR'  {A X φ} : X = ⟨L, R, some (Sum.inr (~'⌊·A⌋(φ : Formula)))⟩ → isBasic X → PdlRule X
-                         ⟨projection A L, (~φ) :: projection A R, none⟩
+  | modL   {A X ξ} : X = ⟨L, R, some (Sum.inl (~'⌊·A⌋(ξ : AnyFormula)))⟩ → isBasic X → PdlRule X
+                         ( match ξ with
+                         | .normal φ => ⟨(~φ) :: projection A L, projection A R, none⟩
+                         | .loaded χ => ⟨projection A L, projection A R, some (Sum.inl (~'χ))⟩ )
+  | modR   {A X ξ} : X = ⟨L, R, some (Sum.inr (~'⌊·A⌋(ξ : AnyFormula)))⟩ → isBasic X → PdlRule X
+                         ( match ξ with
+                         | .normal φ => ⟨projection A L, (~φ) :: projection A R, none⟩
+                         | .loaded χ => ⟨projection A L, projection A R, some (Sum.inr (~'χ))⟩ )
 
 -- ClosedTableau [parent, grandparent, ...] child
 --