L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ φ' ψ' : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
h' : SemanticallyEquivalent T φ' ψ'
⊢ ∀ (M : ModelType T) (v : α → ↑M) (xs : Fin n → ↑M),
    BoundedFormula.Realize φ v xs → BoundedFormula.Realize φ' v xs ↔
      BoundedFormula.Realize ψ v xs → BoundedFormula.Realize ψ' v xs
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ φ' ψ' : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
h' : SemanticallyEquivalent T φ' ψ'
⊢ SemanticallyEquivalent T (φ ⟹ φ') (ψ ⟹ ψ')
simp_rw [SemanticallyEquivalent, ModelsBoundedFormula, BoundedFormula.realize_iff,
  BoundedFormula.realize_imp]
no goals
L : Language
T : Theory L
α : Type w
n : ℕ
φ ψ φ' ψ' : BoundedFormula L α n
h : SemanticallyEquivalent T φ ψ
h' : SemanticallyEquivalent T φ' ψ'
⊢ ∀ (M : ModelType T) (v : α → ↑M) (xs : Fin n → ↑M),
    BoundedFormula.Realize φ v xs → BoundedFormula.Realize φ' v xs ↔
      BoundedFormula.Realize ψ v xs → BoundedFormula.Realize ψ' v xs
exact fun M v xs => imp_congr h.realize_bd_iff h'.realize_bd_iff