subst hq
case mpr.eaxm.inl.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
d : 𝐂𝐥 ⊢! p✝
hEFQ : ∃ p, Axioms.EFQ p = p✝
q : Formula α
hq : Axioms.EFQ q = p✝
⊢ 𝐈𝐧𝐭 ⊢! ~~p✝
case mpr.eaxm.inl.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p q : Formula α
d : 𝐂𝐥 ⊢! Axioms.EFQ q
hEFQ : ∃ p, Axioms.EFQ p = Axioms.EFQ q
⊢ 𝐈𝐧𝐭 ⊢! ~~Axioms.EFQ q