. intro d;
  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 α
⊢ 𝐂𝐥 ⊢! p → 𝐈𝐧𝐭 ⊢! ~~p
no goals