subst hq
case eaxm.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p p✝ : Formula α
h : p✝ ∈ Ax(𝐈𝐧𝐭)
hp : p✝ ∈ theory 𝐈𝐧𝐭
q : Formula α
hq : Axioms.EFQ q = p✝
⊢ 𝐂𝐥 ⊢! p✝
case eaxm.intro
α : Type u
inst✝ : DecidableEq α
𝓓 : DeductionParameter α
p q : Formula α
h : Axioms.EFQ q ∈ Ax(𝐈𝐧𝐭)
hp : Axioms.EFQ q ∈ theory 𝐈𝐧𝐭
⊢ 𝐂𝐥 ⊢! Axioms.EFQ q