L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ BoundedFormula.Realize (φ ⇔ ψ) v xs
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ BoundedFormula.Realize (ψ ⇔ φ) v xs
rw [BoundedFormula.realize_iff, Iff.comm, ← BoundedFormula.realize_iff]
no goals
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
M : ModelType T
v : α → ↑M
xs : Fin n → ↑M
⊢ BoundedFormula.Realize (φ ⇔ ψ) v xs
exact h M v xs