induction h.some using Deduction.inducition_with_nec with
| hMaxm a =>
  rcases a with (hK | hVer)
  . obtain ⟨_, _, e⟩ := hK; subst_vars; dsimp only [Axioms.K, VerTranslation, toPropFormula]; apply imply₁!;
  . obtain ⟨_, e⟩ := hVer; subst_vars; dsimp [Axioms.Ver, VerTranslation, toPropFormula]; exact verum!;
| hMdp h₁ h₂ ih₁ ih₂ =>
  dsimp [VerTranslation, toPropFormula] at ih₁ ih₂;
  exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩);
| hNec => dsimp [toPropFormula]; exact verum!;
| _ =>
  dsimp [VerTranslation, toPropFormula];
  try first
  | apply verum!;
  | apply imply₁!;
  | apply imply₂!;
  | apply conj₁!;
  | apply conj₂!;
  | apply conj₃!;
  | apply disj₁!;
  | apply disj₂!;
  | apply disj₃!;
  | apply dne!;
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐕𝐞𝐫 ⊢! p
⊢ 𝐂𝐥 ⊢! (pⱽᴾ) ⋯
no goals