simp only [eval_disj, eval_neg]
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ eval τ tr ≤ eval τ (disj φ (neg φ))
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ eval τ tr ≤ (eval τ φ || !eval τ φ)