have : [~(q ⋎ ~q)] ⊢[𝐈𝐧𝐭]! ~q ⋏ ~~q := demorgan₃'! $ FiniteContext.id!
case mpr.eaxm.inr.intro.h
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p q : Formula α
d : 𝐂𝐥 ⊢! Axioms.LEM q
hLEM : ∃ p, Axioms.LEM p = Axioms.LEM q
⊢ [~Axioms.LEM q] ⊢[𝐈𝐧𝐭]! Formula.falsum
case mpr.eaxm.inr.intro.h
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p q : Formula α
d : 𝐂𝐥 ⊢! Axioms.LEM q
hLEM : ∃ p, Axioms.LEM p = Axioms.LEM q
this : [~(q ⋎ ~q)] ⊢[𝐈𝐧𝐭]! ~q ⋏ ~~q
⊢ [~Axioms.LEM q] ⊢[𝐈𝐧𝐭]! Formula.falsum