induction h.some with
| eaxm ih =>
  simp_all;
  rcases ih with (efq | lem);
  . obtain ⟨q, e⟩ := efq; subst_vars; exact efq!;
  . obtain ⟨q, e⟩ := lem; subst_vars; exact lem!;
| mdp h₁ h₂ ih₁ ih₂ =>
  dsimp only [Superintuitionistic.Formula.toModalFormula] at ih₁ ih₂;
  exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩);
| _ =>
  dsimp [Superintuitionistic.Formula.toModalFormula];
  try first
  | apply verum!;
  | apply conj₁!;
  | apply conj₂!;
  | apply conj₃!;
  | apply disj₁!;
  | apply disj₂!;
  | apply disj₃!;
  | apply imply₁!;
  | apply imply₂!;
α : Type u_1
inst✝ : DecidableEq α
p✝ : Formula α
m𝓓 : DeductionParameter α
p : Superintuitionistic.Formula α
h : 𝐂𝐥 ⊢! p
⊢ m𝓓 ⊢! pᴹ
no goals