induction h using Deduction.inducition_with_nec! with
| hMaxm hp => exact hMaxm hp;
| hMdp ihpq ihp => exact ihpq ⨀ ihp
| hNec ihp => exact Necessitation.nec! ihp
| _ =>
  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 α
𝓓₁ 𝓓₂ : DeductionParameter α
inst✝¹ : 𝓓₁.Normal
inst✝ : 𝓓₂.Normal
hMaxm : ∀ {p : Formula α}, p ∈ Ax(𝓓₁) → 𝓓₂ ⊢! p
p : Formula α
h : 𝓓₁ ⊢! p
⊢ 𝓓₂ ⊢! p
no goals