have ⟨hnp, hnq⟩ := hC
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬𝐈𝐧𝐭 ⊢! p ∧ ¬𝐈𝐧𝐭 ⊢! q
hnp : ¬𝐈𝐧𝐭 ⊢! p
hnq : ¬𝐈𝐧𝐭 ⊢! q
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q