aesop (add safe le_antisymm)
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ (∀ (τ : PropAssignment ν), eval τ φ₁ = eval τ φ₂) ↔
    (∀ (τ : PropAssignment ν), eval τ φ₁ ≤ eval τ φ₂) ∧ ∀ (τ : PropAssignment ν), eval τ φ₂ ≤ eval τ φ₁
no goals