simp only [eval_disj]
ν✝ : Type u_1
φ₁ φ₃ φ₂ : PropFun ν✝
h₁ : entails φ₁ φ₃
h₂ : entails φ₂ φ₃
τ : PropAssignment ν✝
⊢ eval τ (disj φ₁ φ₂) ≤ eval τ φ₃
ν✝ : Type u_1
φ₁ φ₃ φ₂ : PropFun ν✝
h₁ : entails φ₁ φ₃
h₂ : entails φ₂ φ₃
τ : PropAssignment ν✝
⊢ (eval τ φ₁ || eval τ φ₂) ≤ eval τ φ₃