induction hp.some with
| eaxm h =>
  obtain ⟨q, hq⟩ := by simpa using h;
  subst hq;
  apply efq!;
| mdp h₁ h₂ ih₁ ih₂ => exact (ih₁ ⟨h₁⟩) ⨀ (ih₂ ⟨h₂⟩);
| _ => simp;
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
hp : p ∈ theory 𝐈𝐧𝐭
⊢ 𝐂𝐥 ⊢! p
no goals