The proof scripts using
le_diff'
are exactly the same than for
le_diff
. The proof terms are isomorphic too.
Going home
Pierre Castéran