case of_isQF
L : Language
L' : Language
M : Type w
N : Type ?u.138402
P : Type ?u.138405
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.138433
n l : ℕ
φ✝¹ ψ✝¹ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ✝ : BoundedFormula L α n
hψ✝ : IsPrenex ψ✝
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hφ : IsQF φ✝
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImp φ✝ ψ)

case all
L : Language
L' : Language
M : Type w
N : Type ?u.138402
P : Type ?u.138405
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.138433
n l : ℕ
φ✝¹ ψ✝¹ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ✝ : BoundedFormula L α n
hψ✝ : IsPrenex ψ✝
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
ih1 : ∀ {ψ : BoundedFormula L α (n✝ + 1)}, IsPrenex ψ → IsPrenex (toPrenexImp φ✝ ψ)
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImp (all φ✝) ψ)

case ex
L : Language
L' : Language
M : Type w
N : Type ?u.138402
P : Type ?u.138405
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.138433
n l : ℕ
φ✝¹ ψ✝¹ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ✝ : BoundedFormula L α n
hψ✝ : IsPrenex ψ✝
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
ih2 : ∀ {ψ : BoundedFormula L α (n✝ + 1)}, IsPrenex ψ → IsPrenex (toPrenexImp φ✝ ψ)
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImp (BoundedFormula.ex φ✝) ψ)
L : Language
L' : Language
M : Type w
N : Type ?u.138402
P : Type ?u.138405
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.138433
n l : ℕ
φ✝ ψ✝ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ : BoundedFormula L α n
hφ : IsPrenex φ
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImp φ ψ)
induction' hφ with _ _ hφ _ _ _ ih1 _ _ _ ih2
case of_isQF
L : Language
L' : Language
M : Type w
N : Type ?u.138402
P : Type ?u.138405
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.138433
n l : ℕ
φ✝¹ ψ✝¹ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ✝ : BoundedFormula L α n
hψ✝ : IsPrenex ψ✝
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hφ : IsQF φ✝
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImpRight φ✝ ψ)
case of_isQF
L : Language
L' : Language
M : Type w
N : Type ?u.138402
P : Type ?u.138405
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.138433
n l : ℕ
φ✝¹ ψ✝¹ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ✝ : BoundedFormula L α n
hψ✝ : IsPrenex ψ✝
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hφ : IsQF φ✝
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImp φ✝ ψ)
rw [hφ.toPrenexImp]
no goals
case of_isQF
L : Language
L' : Language
M : Type w
N : Type ?u.138402
P : Type ?u.138405
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.138433
n l : ℕ
φ✝¹ ψ✝¹ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ✝ : BoundedFormula L α n
hψ✝ : IsPrenex ψ✝
n✝ : ℕ
φ✝ : BoundedFormula L α n✝
hφ : IsQF φ✝
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImpRight φ✝ ψ)
exact isPrenex_toPrenexImpRight hφ hψ
no goals
case all
L : Language
L' : Language
M : Type w
N : Type ?u.138402
P : Type ?u.138405
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.138433
n l : ℕ
φ✝¹ ψ✝¹ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ✝ : BoundedFormula L α n
hψ✝ : IsPrenex ψ✝
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
ih1 : ∀ {ψ : BoundedFormula L α (n✝ + 1)}, IsPrenex ψ → IsPrenex (toPrenexImp φ✝ ψ)
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImp (all φ✝) ψ)
exact (ih1 hψ.liftAt).ex
no goals
case ex
L : Language
L' : Language
M : Type w
N : Type ?u.138402
P : Type ?u.138405
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
γ : Type ?u.138433
n l : ℕ
φ✝¹ ψ✝¹ : BoundedFormula L α l
θ : BoundedFormula L α (Nat.succ l)
v : α → M
xs : Fin l → M
φ ψ✝ : BoundedFormula L α n
hψ✝ : IsPrenex ψ✝
n✝ : ℕ
φ✝ : BoundedFormula L α (n✝ + 1)
h✝ : IsPrenex φ✝
ih2 : ∀ {ψ : BoundedFormula L α (n✝ + 1)}, IsPrenex ψ → IsPrenex (toPrenexImp φ✝ ψ)
ψ : BoundedFormula L α n✝
hψ : IsPrenex ψ
⊢ IsPrenex (toPrenexImp (BoundedFormula.ex φ✝) ψ)
exact (ih2 hψ.liftAt).all