∀[f,x:Base]. f(x) ≤ f x supposing ¬is-exception(f(x))
{ (Auto THEN All (Unfold `ml_apply`)) }
1. f : Base
2. x : Base
3. ¬is-exception(let y ⟵ x
in f y)
4. (let y ⟵ x
in f y)↓
⊢ let y ⟵ x
in f y ≤ f x