induction h using Deduction.inducition! with
| hMaxm hp =>
  rcases hp with (hK | hL)
  . obtain ⟨_, _, e⟩ := hK; subst_vars; exact axiomK!;
  . obtain ⟨_, e⟩ := hL; subst_vars; exact axiomL!;
| hMdp ihpq ihp => exact ihpq ⨀ ihp;
| hNec _ ihp => exact Necessitation.nec! ihp;
| hLoeb _ ihp => exact LoebRule.loeb! ihp;
| hHenkin => simp_all only [Bool.false_eq_true];
| _ =>
  try first
  | apply verum!;
  | apply imply₁!;
  | apply imply₂!;
  | apply conj₁!;
  | apply conj₂!;
  | apply conj₃!;
  | apply disj₁!;
  | apply disj₂!;
  | apply disj₃!;
  | apply dne!;
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐆𝐋 ⊢! p
⊢ 𝐊𝟒(𝐋) ⊢! p
no goals