intro hC
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
⊢ ¬(𝐈𝐧𝐭 ⊢! p ∨ 𝐈𝐧𝐭 ⊢! q) → ¬𝐈𝐧𝐭 ⊢! p ⋎ q
α : Type u_1
inst✝² : Inhabited α
inst✝¹ : DecidableEq α
inst✝ : Encodable α
p q : Formula α
M₁ M₂ : Model α
hC : ¬(𝐈𝐧𝐭 ⊢! p ∨ 𝐈𝐧𝐭 ⊢! q)
⊢ ¬𝐈𝐧𝐭 ⊢! p ⋎ q