induction d.some with
| eaxm h =>
  simp at h;
  rcases h with (hEFQ | hLEM);
  . obtain ⟨q, hq⟩ := by simpa using hEFQ;
    subst hq;
    exact dni'! efq!;
  . obtain ⟨q, hq⟩ := by simpa using hLEM;
    subst hq;
    apply FiniteContext.deduct'!;
    have : [~(q ⋎ ~q)] ⊢[𝐈𝐧𝐭]! ~q ⋏ ~~q := demorgan₃'! $ FiniteContext.id!;
    exact (conj₂'! this) ⨀ (conj₁'! this);
| @mdp p q h₁ h₂ ih₁ ih₂ =>
  exact (dn_distribute_imply'! $ ih₁ ⟨h₁⟩) ⨀ ih₂ ⟨h₂⟩;
| _ => apply dni'!; simp;
case mpr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p : Formula α
d : 𝐂𝐥 ⊢! p
⊢ 𝐈𝐧𝐭 ⊢! ~~p
no goals