English
For prenex φ and ψ, (φ.toPrenexImp ψ).Realize equals (φ.imp ψ).Realize.
Русский
Для пренекс φ и ψ, реализации равны между (φ.toPrenexImp ψ) и (φ.imp ψ).
LaTeX
$$$(φ.toPrenexImp ψ).Realize v xs \leftrightarrow (φ.imp ψ).Realize v xs$$$
Lean4
theorem realize_toPrenexImp {φ ψ : L.BoundedFormula α n} (hφ : IsPrenex φ) (hψ : IsPrenex ψ) {v : α → M}
{xs : Fin n → M} : (φ.toPrenexImp ψ).Realize v xs ↔ (φ.imp ψ).Realize v xs :=
by
revert ψ
induction hφ with
| of_isQF hφ =>
intro ψ hψ
rw [hφ.toPrenexImp]
exact realize_toPrenexImpRight hφ hψ
| all _ ih =>
intro ψ hψ
unfold toPrenexImp
rw [realize_ex]
refine _root_.trans (exists_congr fun _ => ih hψ.liftAt) ?_
simp only [realize_imp, realize_liftAt_one_self, snoc_comp_castSucc, realize_all]
exact Iff.symm forall_imp_iff_exists_imp
| ex _ ih =>
intro ψ hψ
refine _root_.trans (forall_congr' fun _ => ih hψ.liftAt) ?_
simp
