existsi (Axioms.L (atom default))
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ f, 𝐆𝐋 ⊢! f ∧ 𝐊𝟒 ⊬! f
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊢! Axioms.L (atom default) ∧ 𝐊𝟒 ⊬! Axioms.L (atom default)