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