Thanks, that worked great.I was a bit puzzled about why there is no lemma that states that theâ âproper subsetâ relation on finite sets is well-founded. I'll add that to the library.
It would be nice to generalise the Min/Max operators to also work with non-linear orders. ArgMin/ArgMax would also be really useful.
Any opinions on that? Cheers, Manuel