case of_isAtomic
L : Language
L' : Language
M : Type w
N : Type ?u.113613
P : Type ?u.113616
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.113644
n l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ : BoundedFormula L α (n + 1)
con : IsAtomic (all φ)
⊢ False
L : Language
L' : Language
M : Type w
N : Type ?u.113613
P : Type ?u.113616
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.113644
n l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ : BoundedFormula L α (n + 1)
con : IsQF (all φ)
⊢ False
cases' con with _ con
no goals
case of_isAtomic
L : Language
L' : Language
M : Type w
N : Type ?u.113613
P : Type ?u.113616
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.113644
n l : ℕ
φ✝ ψ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ : BoundedFormula L α (n + 1)
con : IsAtomic (all φ)
⊢ False
exact φ.not_all_isAtomic con