simp only [true_implies]
case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ true = true → eval τ φ₂ = true ↔ true ≤ eval τ φ₂
case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ eval τ φ₂ = true ↔ true ≤ eval τ φ₂