by_contra hC
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
⊢ 𝐈𝐧𝐭 ⊬! p ⋎ ~p
case intro
α : Type
inst✝ : Inhabited α
p : Formula α
h✝ : ¬𝔽(Ax(𝐈𝐧𝐭)) ⊧ p ⋎ ~p
hC : 𝐈𝐧𝐭 ⊢! p ⋎ ~p
⊢ False