induction h.some using Deduction.inducition_with_nec with
| hMaxm a =>
  rcases a with (hK | hT) | hTc;
  . obtain ⟨_, _, e⟩ := hK; subst_vars; dsimp [Axioms.K, TrivTranslation, toPropFormula]; apply imp_id!;
  . obtain ⟨_, e⟩ := hT; subst_vars; dsimp [Axioms.T, TrivTranslation, toPropFormula]; apply imp_id!;
  . obtain ⟨_, e⟩ := hTc; subst_vars; dsimp [Axioms.Tc, TrivTranslation, toPropFormula]; apply imp_id!;
| hMdp h₁ h₂ ih₁ ih₂ =>
  dsimp [TrivTranslation, toPropFormula] at ih₁ ih₂;
  exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩);
| hNec _ ih => exact ih $ axiomT'! h;
| _ =>
  dsimp [TrivTranslation, toPropFormula];
  try first
  | apply imp_id!;
  | apply verum!;
  | apply conj₁!;
  | apply conj₂!;
  | apply conj₃!;
  | apply disj₁!;
  | apply disj₂!;
  | apply disj₃!;
  | apply imply₁!;
  | apply imply₂!;
  | apply dne!;
case mp
α : Type u_1
inst✝ : DecidableEq α
p : Formula α
h : 𝐓𝐫𝐢𝐯 ⊢! p
⊢ 𝐂𝐥 ⊢! (pᵀᴾ) ⋯
no goals