have : ∀ τ, (φ₁.eval τ → φ₂.eval τ) ↔ φ₁.eval τ ≤ φ₂.eval τ := by
  intro τ
  cases (eval τ φ₁)
  . simp
  . simp only [true_implies]
    exact ⟨fun h => h ▸ le_rfl, top_unique⟩
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
this : ∀ (τ : PropAssignment ν), eval τ φ₁ = true → eval τ φ₂ = true ↔ eval τ φ₁ ≤ eval τ φ₂
⊢ entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂