. 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);
case mpr.eaxm.inr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hLEM : ∃ p, Axioms.LEM p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝
no goals