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