have ⟨φ₁, h₁⟩ := Quotient.exists_rep φ₁
ν : Type u_1
φ₁ φ₂ : PropFun ν
⊢ entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂
ν : Type u_1
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ entails φ₁✝ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁✝ → τ ⊨ φ₂