Function value_le 

pub fn value_le<X: Term, Y: Term>(
    x: Value<X>,
    y: Value<Y>,
) -> Option<ValueLe<X, Y>>
where
    X::Type: PartialOrd<Y::Type> + Ord,
    Y::Type: Ord,

Return evidence of x <= y