have : L ⊢! p := dne'! $ replace_imply_left_conj'! hΓ hC
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 = p ⟶ ⊥
hC : L ⊢! Γ.conj' ⟶ ⊥
⊢ False
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Inhabited α
L : DeductionParameter α
inst✝¹ : L.Normal
inst✝ : Inhabited (MCT L)
p : Formula α
h : ¬L ⊢! p
Γ : List (Formula α)
hΓ : ∀ p_1 ∈ Γ, p_1 = p ⟶ ⊥
hC : L ⊢! Γ.conj' ⟶ ⊥
this : L ⊢! p
⊢ False