Theorem: LeanSAT.Model.PropForm.equivalent_ext (LeanSAT/Model/PropForm.lean)

State before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ equivalent φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ ↔ τ ⊨ φ₂
Tactic:
simp only [equivalent_iff_entails, entails_ext]
State after:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ ((∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂) ∧ ∀ (τ : PropAssignment ν), τ ⊨ φ₂ → τ ⊨ φ₁) ↔
    ∀ (τ : PropAssignment ν), τ ⊨ φ₁ ↔ τ ⊨ φ₂

State before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ ((∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂) ∧ ∀ (τ : PropAssignment ν), τ ⊨ φ₂ → τ ⊨ φ₁) ↔
    ∀ (τ : PropAssignment ν), τ ⊨ φ₁ ↔ τ ⊨ φ₂
Tactic:
aesop
State after:
no goals