induction h.some using Deduction.inducition_with_nec with
| hMaxm a =>
  rcases a with (hK | hT) | hFour;
  . obtain ⟨_, _, e⟩ := hK; subst_vars; dsimp [Axioms.K, BoxdotTranslation]; apply boxdot_axiomK!;
  . obtain ⟨_, e⟩ := hT; subst_vars; dsimp [Axioms.T, BoxdotTranslation]; apply boxdot_axiomT!;
  . obtain ⟨_, e⟩ := hFour; subst_vars; dsimp [Axioms.Four, BoxdotTranslation]; apply boxdot_axiomFour!;
| hNec hp ihp =>
  dsimp [BoxdotTranslation];
  exact boxdot_nec! $ ihp ⟨hp⟩;
| hMdp hpq hp ihpq ihp =>
  dsimp [BoxdotTranslation] at ihpq ihp;
  exact (ihpq ⟨hpq⟩) ⨀ (ihp ⟨hp⟩);
| _ =>
  dsimp [BoxdotTranslation];
  try first
  | apply verum!;
  | apply conj₁!;
  | apply conj₂!;
  | apply conj₃!;
  | apply disj₁!;
  | apply disj₂!;
  | apply disj₃!;
  | apply imply₁!;
  | apply imply₂!;
  | apply dne!;
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐒𝟒 ⊢! p
⊢ 𝐊𝟒 ⊢! pᵇ
no goals