rcases h with (hEFQ | hLEM)
case mpr.eaxm
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
h : (∃ p, Axioms.EFQ p = p✝) ∨ ∃ p, Axioms.LEM p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝
case mpr.eaxm.inl
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hEFQ : ∃ p, Axioms.EFQ p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝

case mpr.eaxm.inr
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hLEM : ∃ p, Axioms.LEM p = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝