fix

LabelledSystem.lean

@@ -2,3 +2,4 @@ import LabelledSystem.Basic
 
 import LabelledSystem.Gentzen.Basic
 import LabelledSystem.Gentzen.Soundness
+import LabelledSystem.Gentzen.Hilbert

LabelledSystem/Gentzen/Hilbert.lean

@@ -56,8 +56,8 @@ def axiomK : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ □(φ ➝ ψ) ➝ □φ ➝ 
     have e : (x ∶ □(φ ➝ ψ)) ::ₘ (y ∶ φ ➝ ψ) ::ₘ (y ∶ φ) ::ₘ {x ∶ □φ} = (y ∶ φ ➝ ψ) ::ₘ {y ∶ φ, x ∶ □φ, x ∶ □(φ ➝ ψ)} := by sorry;
     simpa [e];
   apply impL (Γ := ⟨_, _⟩);
-  . simpa using initFml (Γ := ⟨_, _⟩) (Δ := ⟨_, _⟩);
-  . simpa using initFml (Γ := ⟨_, _⟩) (Δ := ⟨_, _⟩);
+  . exact initFml' y φ (by simp) (by simp);
+  . exact initFml' y ψ (by simp) (by simp);
 
 def mdp (d₁ : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ φ ➝ ψ}, ∅⟩) (d₂ : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ φ}, ∅⟩) : ⊢ᵍ ⟨∅, ∅⟩ ⟹ ⟨{x ∶ ψ}, ∅⟩ := by
   simpa using cutFml (Δ₁ := ⟨∅, ∅⟩) (Δ₂ := ⟨{x ∶ ψ}, ∅⟩) d₂ $ implyRInv (Δ := ⟨∅, ∅⟩) d₁;

LabelledSystem/Gentzen/Soundness.lean

@@ -5,10 +5,10 @@ namespace LO.Modal.Labelled.Gentzen
 theorem soundness {S : Sequent} : ⊢ᵍ S → ∀ (M : Kripke.Model), ∀ (f : Assignment M), S.Satisfies M f := by
   intro d;
   induction d with
-  | axA =>
+  | initAtom =>
     rintro M f ⟨hΓ, hX⟩;
     simp_all;
-  | axBot =>
+  | initBot =>
     rintro M f ⟨hΓ, hX⟩;
     simp at hΓ;
   | @impL Γ Δ x φ ψ d₁ d₂ ih₁ ih₂ =>