exact imp_trans! hC efq! ⨀ (by
  apply iff_provable_list_conj.mpr;
  exact λ _ hp => ⟨Deduction.eaxm $ hΓ _ hp⟩;
)
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
𝓓 : DeductionParameter α
inst✝¹ : 𝓓.IncludeEFQ
inst✝ : Inhabited α
h : Consistent 𝓓
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ (Ax(𝓓), ∅).1
q : Formula α
hq : 𝓓 ⊬! q
hC : 𝓓 ⊢! Γ.conj' ⟶ ⊥
⊢ 𝓓 ⊢! q
no goals